YES 112.279 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule FiniteMap
  ((filterFM :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a) :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
  addToFM :: Ord a => FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM fm key elt = addToFM_C (\old new ->new) fm key elt

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt 
 | new_key < key = 
mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key = 
mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise = 
Branch new_key (combiner elt new_elt) size fm_l fm_r

  deleteMax :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMax (Branch key elt _ fm_l EmptyFM) = fm_l
deleteMax (Branch key elt _ fm_l fm_r) = mkBalBranch key elt fm_l (deleteMax fm_r)

  deleteMin :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMin (Branch key elt _ EmptyFM fm_r) = fm_r
deleteMin (Branch key elt _ fm_l fm_r) = mkBalBranch key elt (deleteMin fm_l) fm_r

  emptyFM :: FiniteMap a b
emptyFM = EmptyFM

  filterFM :: Ord b => (b  ->  a  ->  Bool)  ->  FiniteMap b a  ->  FiniteMap b a
filterFM p EmptyFM = emptyFM
filterFM p (Branch key elt _ fm_l fm_r) 
 | p key elt = 
mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
 | otherwise = 
glueVBal (filterFM p fm_l) (filterFM p fm_r)

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt _ _ EmptyFM) = (key,elt)
findMax (Branch key elt _ _ fm_r) = findMax fm_r

  findMin :: FiniteMap b a  ->  (b,a)
findMin (Branch key elt _ EmptyFM _) = (key,elt)
findMin (Branch key elt _ fm_l _) = findMin fm_l

  glueBal :: Ord b => FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
glueBal EmptyFM fm2 = fm2
glueBal fm1 EmptyFM = fm1
glueBal fm1 fm2 
 | sizeFM fm2 > sizeFM fm1 = 
mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2)
 | otherwise = 
mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2 where 
mid_elt1 = (\(_,mid_elt1) ->mid_elt1) vv2
mid_elt2 = (\(_,mid_elt2) ->mid_elt2) vv3
mid_key1 = (\(mid_key1,_) ->mid_key1) vv2
mid_key2 = (\(mid_key2,_) ->mid_key2) vv3
vv2 = findMax fm1
vv3 = findMin fm2

  glueVBal :: Ord b => FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
glueVBal EmptyFM fm2 = fm2
glueVBal fm1 EmptyFM = fm1
glueVBal fm_l@(Branch key_l elt_l _ fm_ll fm_lr) fm_r@(Branch key_r elt_r _ fm_rl fm_rr) 
 | sIZE_RATIO * size_l < size_r = 
mkBalBranch key_r elt_r (glueVBal fm_l fm_rl) fm_rr
 | sIZE_RATIO * size_r < size_l = 
mkBalBranch key_l elt_l fm_ll (glueVBal fm_lr fm_r)
 | otherwise = 
glueBal fm_l fm_r where 
size_l = sizeFM fm_l
size_r = sizeFM fm_r

  mkBalBranch :: Ord b => b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBalBranch key elt fm_L fm_R 
 | size_l + size_r < 2 = 
mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l = 
case fm_R of
  Branch _ _ _ fm_rl fm_rr
 | sizeFM fm_rl < 2 * sizeFM fm_rr -> 
single_L fm_L fm_R
 | otherwise -> 
double_L fm_L fm_R
 | size_l > sIZE_RATIO * size_r = 
case fm_L of
  Branch _ _ _ fm_ll fm_lr
 | sizeFM fm_lr < 2 * sizeFM fm_ll -> 
single_R fm_L fm_R
 | otherwise -> 
double_R fm_L fm_R
 | otherwise = 
mkBranch 2 key elt fm_L fm_R where 
double_L fm_l (Branch key_r elt_r _ (Branch key_rl elt_rl _ fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l _ fm_ll (Branch key_lr elt_lr _ fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
single_L fm_l (Branch key_r elt_r _ fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l _ fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord a => Int  ->  a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = 
case fm_l of
  EmptyFM-> True
  Branch left_key _ _ _ _-> 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = 
case fm_r of
  EmptyFM-> True
  Branch right_key _ _ _ _-> 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  mkVBalBranch :: Ord b => b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkVBalBranch key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch key elt fm_l@(Branch key_l elt_l _ fm_ll fm_lr) fm_r@(Branch key_r elt_r _ fm_rl fm_rr) 
 | sIZE_RATIO * size_l < size_r = 
mkBalBranch key_r elt_r (mkVBalBranch key elt fm_l fm_rl) fm_rr
 | sIZE_RATIO * size_r < size_l = 
mkBalBranch key_l elt_l fm_ll (mkVBalBranch key elt fm_lr fm_r)
 | otherwise = 
mkBranch 13 key elt fm_l fm_r where 
size_l = sizeFM fm_l
size_r = sizeFM fm_r

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size

  unitFM :: b  ->  a  ->  FiniteMap b a
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\(mid_key1,_)→mid_key1

is transformed to
mid_key10 (mid_key1,_) = mid_key1

The following Lambda expression
\(_,mid_elt1)→mid_elt1

is transformed to
mid_elt10 (_,mid_elt1) = mid_elt1

The following Lambda expression
\(mid_key2,_)→mid_key2

is transformed to
mid_key20 (mid_key2,_) = mid_key2

The following Lambda expression
\(_,mid_elt2)→mid_elt2

is transformed to
mid_elt20 (_,mid_elt2) = mid_elt2

The following Lambda expression
\oldnew→new

is transformed to
addToFM0 old new = new



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR

mainModule FiniteMap
  ((filterFM :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a) :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt 
 | new_key < key = 
mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key = 
mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise = 
Branch new_key (combiner elt new_elt) size fm_l fm_r

  deleteMax :: Ord b => FiniteMap b a  ->  FiniteMap b a
deleteMax (Branch key elt _ fm_l EmptyFM) = fm_l
deleteMax (Branch key elt _ fm_l fm_r) = mkBalBranch key elt fm_l (deleteMax fm_r)

  deleteMin :: Ord b => FiniteMap b a  ->  FiniteMap b a
deleteMin (Branch key elt _ EmptyFM fm_r) = fm_r
deleteMin (Branch key elt _ fm_l fm_r) = mkBalBranch key elt (deleteMin fm_l) fm_r

  emptyFM :: FiniteMap b a
emptyFM = EmptyFM

  filterFM :: Ord b => (b  ->  a  ->  Bool)  ->  FiniteMap b a  ->  FiniteMap b a
filterFM p EmptyFM = emptyFM
filterFM p (Branch key elt _ fm_l fm_r) 
 | p key elt = 
mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
 | otherwise = 
glueVBal (filterFM p fm_l) (filterFM p fm_r)

  findMax :: FiniteMap a b  ->  (a,b)
findMax (Branch key elt _ _ EmptyFM) = (key,elt)
findMax (Branch key elt _ _ fm_r) = findMax fm_r

  findMin :: FiniteMap a b  ->  (a,b)
findMin (Branch key elt _ EmptyFM _) = (key,elt)
findMin (Branch key elt _ fm_l _) = findMin fm_l

  glueBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueBal EmptyFM fm2 = fm2
glueBal fm1 EmptyFM = fm1
glueBal fm1 fm2 
 | sizeFM fm2 > sizeFM fm1 = 
mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2)
 | otherwise = 
mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2 where 
mid_elt1 = mid_elt10 vv2
mid_elt10 (_,mid_elt1) = mid_elt1
mid_elt2 = mid_elt20 vv3
mid_elt20 (_,mid_elt2) = mid_elt2
mid_key1 = mid_key10 vv2
mid_key10 (mid_key1,_) = mid_key1
mid_key2 = mid_key20 vv3
mid_key20 (mid_key2,_) = mid_key2
vv2 = findMax fm1
vv3 = findMin fm2

  glueVBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueVBal EmptyFM fm2 = fm2
glueVBal fm1 EmptyFM = fm1
glueVBal fm_l@(Branch key_l elt_l _ fm_ll fm_lr) fm_r@(Branch key_r elt_r _ fm_rl fm_rr) 
 | sIZE_RATIO * size_l < size_r = 
mkBalBranch key_r elt_r (glueVBal fm_l fm_rl) fm_rr
 | sIZE_RATIO * size_r < size_l = 
mkBalBranch key_l elt_l fm_ll (glueVBal fm_lr fm_r)
 | otherwise = 
glueBal fm_l fm_r where 
size_l = sizeFM fm_l
size_r = sizeFM fm_r

  mkBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBalBranch key elt fm_L fm_R 
 | size_l + size_r < 2 = 
mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l = 
case fm_R of
  Branch _ _ _ fm_rl fm_rr
 | sizeFM fm_rl < 2 * sizeFM fm_rr -> 
single_L fm_L fm_R
 | otherwise -> 
double_L fm_L fm_R
 | size_l > sIZE_RATIO * size_r = 
case fm_L of
  Branch _ _ _ fm_ll fm_lr
 | sizeFM fm_lr < 2 * sizeFM fm_ll -> 
single_R fm_L fm_R
 | otherwise -> 
double_R fm_L fm_R
 | otherwise = 
mkBranch 2 key elt fm_L fm_R where 
double_L fm_l (Branch key_r elt_r _ (Branch key_rl elt_rl _ fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l _ fm_ll (Branch key_lr elt_lr _ fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
single_L fm_l (Branch key_r elt_r _ fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l _ fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord a => Int  ->  a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = 
case fm_l of
  EmptyFM-> True
  Branch left_key _ _ _ _-> 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = 
case fm_r of
  EmptyFM-> True
  Branch right_key _ _ _ _-> 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  mkVBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkVBalBranch key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch key elt fm_l@(Branch key_l elt_l _ fm_ll fm_lr) fm_r@(Branch key_r elt_r _ fm_rl fm_rr) 
 | sIZE_RATIO * size_l < size_r = 
mkBalBranch key_r elt_r (mkVBalBranch key elt fm_l fm_rl) fm_rr
 | sIZE_RATIO * size_r < size_l = 
mkBalBranch key_l elt_l fm_ll (mkVBalBranch key elt fm_lr fm_r)
 | otherwise = 
mkBranch 13 key elt fm_l fm_r where 
size_l = sizeFM fm_l
size_r = sizeFM fm_r

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size

  unitFM :: b  ->  a  ->  FiniteMap b a
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Case Reductions:
The following Case expression
case fm_l of
 EmptyFM → True
 Branch left_key _ _ _ _ → 
let 
biggest_left_key  = fst (findMax fm_l)
in biggest_left_key < key

is transformed to
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key _ _ _ _) = 
let 
biggest_left_key  = fst (findMax fm_l)
in biggest_left_key < key

The following Case expression
case fm_r of
 EmptyFM → True
 Branch right_key _ _ _ _ → 
let 
smallest_right_key  = fst (findMin fm_r)
in key < smallest_right_key

is transformed to
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key _ _ _ _) = 
let 
smallest_right_key  = fst (findMin fm_r)
in key < smallest_right_key

The following Case expression
case fm_R of
 Branch _ _ _ fm_rl fm_rr
 | sizeFM fm_rl < 2 * sizeFM fm_rr
 → single_L fm_L fm_R
 | otherwise
 → double_L fm_L fm_R

is transformed to
mkBalBranch0 fm_L fm_R (Branch _ _ _ fm_rl fm_rr)
 | sizeFM fm_rl < 2 * sizeFM fm_rr
 = single_L fm_L fm_R
 | otherwise
 = double_L fm_L fm_R

The following Case expression
case fm_L of
 Branch _ _ _ fm_ll fm_lr
 | sizeFM fm_lr < 2 * sizeFM fm_ll
 → single_R fm_L fm_R
 | otherwise
 → double_R fm_L fm_R

is transformed to
mkBalBranch1 fm_L fm_R (Branch _ _ _ fm_ll fm_lr)
 | sizeFM fm_lr < 2 * sizeFM fm_ll
 = single_R fm_L fm_R
 | otherwise
 = double_R fm_L fm_R



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR

mainModule FiniteMap
  ((filterFM :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a) :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord a => (b  ->  b  ->  b)  ->  FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt 
 | new_key < key = 
mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key = 
mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise = 
Branch new_key (combiner elt new_elt) size fm_l fm_r

  deleteMax :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMax (Branch key elt _ fm_l EmptyFM) = fm_l
deleteMax (Branch key elt _ fm_l fm_r) = mkBalBranch key elt fm_l (deleteMax fm_r)

  deleteMin :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMin (Branch key elt _ EmptyFM fm_r) = fm_r
deleteMin (Branch key elt _ fm_l fm_r) = mkBalBranch key elt (deleteMin fm_l) fm_r

  emptyFM :: FiniteMap a b
emptyFM = EmptyFM

  filterFM :: Ord b => (b  ->  a  ->  Bool)  ->  FiniteMap b a  ->  FiniteMap b a
filterFM p EmptyFM = emptyFM
filterFM p (Branch key elt _ fm_l fm_r) 
 | p key elt = 
mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
 | otherwise = 
glueVBal (filterFM p fm_l) (filterFM p fm_r)

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt _ _ EmptyFM) = (key,elt)
findMax (Branch key elt _ _ fm_r) = findMax fm_r

  findMin :: FiniteMap b a  ->  (b,a)
findMin (Branch key elt _ EmptyFM _) = (key,elt)
findMin (Branch key elt _ fm_l _) = findMin fm_l

  glueBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueBal EmptyFM fm2 = fm2
glueBal fm1 EmptyFM = fm1
glueBal fm1 fm2 
 | sizeFM fm2 > sizeFM fm1 = 
mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2)
 | otherwise = 
mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2 where 
mid_elt1 = mid_elt10 vv2
mid_elt10 (_,mid_elt1) = mid_elt1
mid_elt2 = mid_elt20 vv3
mid_elt20 (_,mid_elt2) = mid_elt2
mid_key1 = mid_key10 vv2
mid_key10 (mid_key1,_) = mid_key1
mid_key2 = mid_key20 vv3
mid_key20 (mid_key2,_) = mid_key2
vv2 = findMax fm1
vv3 = findMin fm2

  glueVBal :: Ord b => FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
glueVBal EmptyFM fm2 = fm2
glueVBal fm1 EmptyFM = fm1
glueVBal fm_l@(Branch key_l elt_l _ fm_ll fm_lr) fm_r@(Branch key_r elt_r _ fm_rl fm_rr) 
 | sIZE_RATIO * size_l < size_r = 
mkBalBranch key_r elt_r (glueVBal fm_l fm_rl) fm_rr
 | sIZE_RATIO * size_r < size_l = 
mkBalBranch key_l elt_l fm_ll (glueVBal fm_lr fm_r)
 | otherwise = 
glueBal fm_l fm_r where 
size_l = sizeFM fm_l
size_r = sizeFM fm_r

  mkBalBranch :: Ord b => b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBalBranch key elt fm_L fm_R 
 | size_l + size_r < 2 = 
mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l = 
mkBalBranch0 fm_L fm_R fm_R
 | size_l > sIZE_RATIO * size_r = 
mkBalBranch1 fm_L fm_R fm_L
 | otherwise = 
mkBranch 2 key elt fm_L fm_R where 
double_L fm_l (Branch key_r elt_r _ (Branch key_rl elt_rl _ fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l _ fm_ll (Branch key_lr elt_lr _ fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch _ _ _ fm_rl fm_rr) 
 | sizeFM fm_rl < 2 * sizeFM fm_rr = 
single_L fm_L fm_R
 | otherwise = 
double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch _ _ _ fm_ll fm_lr) 
 | sizeFM fm_lr < 2 * sizeFM fm_ll = 
single_R fm_L fm_R
 | otherwise = 
double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r _ fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l _ fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord a => Int  ->  a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key _ _ _ _) = 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key _ _ _ _) = 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  mkVBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkVBalBranch key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch key elt fm_l@(Branch key_l elt_l _ fm_ll fm_lr) fm_r@(Branch key_r elt_r _ fm_rl fm_rr) 
 | sIZE_RATIO * size_l < size_r = 
mkBalBranch key_r elt_r (mkVBalBranch key elt fm_l fm_rl) fm_rr
 | sIZE_RATIO * size_r < size_l = 
mkBalBranch key_l elt_l fm_ll (mkVBalBranch key elt fm_lr fm_r)
 | otherwise = 
mkBranch 13 key elt fm_l fm_r where 
size_l = sizeFM fm_l
size_r = sizeFM fm_r

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch _ _ size _ _) = size

  unitFM :: b  ->  a  ->  FiniteMap b a
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
fm_l@(Branch yv yw yx yy yz)

is replaced by the following term
Branch yv yw yx yy yz

The bind variable of the following binding Pattern
fm_r@(Branch zv zw zx zy zz)

is replaced by the following term
Branch zv zw zx zy zz

The bind variable of the following binding Pattern
fm_l@(Branch vux vuy vuz vvu vvv)

is replaced by the following term
Branch vux vuy vuz vvu vvv

The bind variable of the following binding Pattern
fm_r@(Branch vvx vvy vvz vwu vwv)

is replaced by the following term
Branch vvx vvy vvz vwu vwv



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR

mainModule FiniteMap
  ((filterFM :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a) :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
  addToFM :: Ord a => FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord a => (b  ->  b  ->  b)  ->  FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt 
 | new_key < key = 
mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key = 
mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise = 
Branch new_key (combiner elt new_elt) size fm_l fm_r

  deleteMax :: Ord b => FiniteMap b a  ->  FiniteMap b a
deleteMax (Branch key elt vuu fm_l EmptyFM) = fm_l
deleteMax (Branch key elt vuv fm_l fm_r) = mkBalBranch key elt fm_l (deleteMax fm_r)

  deleteMin :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMin (Branch key elt vzy EmptyFM fm_r) = fm_r
deleteMin (Branch key elt vzz fm_l fm_r) = mkBalBranch key elt (deleteMin fm_l) fm_r

  emptyFM :: FiniteMap a b
emptyFM = EmptyFM

  filterFM :: Ord a => (a  ->  b  ->  Bool)  ->  FiniteMap a b  ->  FiniteMap a b
filterFM p EmptyFM = emptyFM
filterFM p (Branch key elt wuu fm_l fm_r) 
 | p key elt = 
mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
 | otherwise = 
glueVBal (filterFM p fm_l) (filterFM p fm_r)

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt vzu vzv EmptyFM) = (key,elt)
findMax (Branch key elt vzw vzx fm_r) = findMax fm_r

  findMin :: FiniteMap a b  ->  (a,b)
findMin (Branch key elt wy EmptyFM wz) = (key,elt)
findMin (Branch key elt xu fm_l xv) = findMin fm_l

  glueBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueBal EmptyFM fm2 = fm2
glueBal fm1 EmptyFM = fm1
glueBal fm1 fm2 
 | sizeFM fm2 > sizeFM fm1 = 
mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2)
 | otherwise = 
mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2 where 
mid_elt1 = mid_elt10 vv2
mid_elt10 (vyw,mid_elt1) = mid_elt1
mid_elt2 = mid_elt20 vv3
mid_elt20 (vyx,mid_elt2) = mid_elt2
mid_key1 = mid_key10 vv2
mid_key10 (mid_key1,vyy) = mid_key1
mid_key2 = mid_key20 vv3
mid_key20 (mid_key2,vyz) = mid_key2
vv2 = findMax fm1
vv3 = findMin fm2

  glueVBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueVBal EmptyFM fm2 = fm2
glueVBal fm1 EmptyFM = fm1
glueVBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) 
 | sIZE_RATIO * size_l < size_r = 
mkBalBranch zv zw (glueVBal (Branch yv yw yx yy yz) zy) zz
 | sIZE_RATIO * size_r < size_l = 
mkBalBranch yv yw yy (glueVBal yz (Branch zv zw zx zy zz))
 | otherwise = 
glueBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) where 
size_l = sizeFM (Branch yv yw yx yy yz)
size_r = sizeFM (Branch zv zw zx zy zz)

  mkBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBalBranch key elt fm_L fm_R 
 | size_l + size_r < 2 = 
mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l = 
mkBalBranch0 fm_L fm_R fm_R
 | size_l > sIZE_RATIO * size_r = 
mkBalBranch1 fm_L fm_R fm_L
 | otherwise = 
mkBranch 2 key elt fm_L fm_R where 
double_L fm_l (Branch key_r elt_r vxw (Branch key_rl elt_rl vxx fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vxu fm_ll (Branch key_lr elt_lr vxv fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) 
 | sizeFM fm_rl < 2 * sizeFM fm_rr = 
single_L fm_L fm_R
 | otherwise = 
double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) 
 | sizeFM fm_lr < 2 * sizeFM fm_ll = 
single_R fm_L fm_R
 | otherwise = 
double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r vyv fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vww fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key wu wv ww wx) = 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key vw vx vy vz) = 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  mkVBalBranch :: Ord b => b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkVBalBranch key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) 
 | sIZE_RATIO * size_l < size_r = 
mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv
 | sIZE_RATIO * size_r < size_l = 
mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv))
 | otherwise = 
mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) where 
size_l = sizeFM (Branch vux vuy vuz vvu vvv)
size_r = sizeFM (Branch vvx vvy vvz vwu vwv)

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch xw xx size xy xz) = size

  unitFM :: a  ->  b  ->  FiniteMap a b
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Cond Reductions:
The following Function with conditions
glueVBal EmptyFM fm2 = fm2
glueVBal fm1 EmptyFM = fm1
glueVBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)
 | sIZE_RATIO * size_l < size_r
 = mkBalBranch zv zw (glueVBal (Branch yv yw yx yy yz) zy) zz
 | sIZE_RATIO * size_r < size_l
 = mkBalBranch yv yw yy (glueVBal yz (Branch zv zw zx zy zz))
 | otherwise
 = glueBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)
where 
size_l  = sizeFM (Branch yv yw yx yy yz)
size_r  = sizeFM (Branch zv zw zx zy zz)

is transformed to
glueVBal EmptyFM fm2 = glueVBal5 EmptyFM fm2
glueVBal fm1 EmptyFM = glueVBal4 fm1 EmptyFM
glueVBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) = glueVBal3 (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)

glueVBal3 (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) = 
glueVBal2 yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * size_l < size_r)
where 
glueVBal0 yv yw yx yy yz zv zw zx zy zz True = glueBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)
glueVBal1 yv yw yx yy yz zv zw zx zy zz True = mkBalBranch yv yw yy (glueVBal yz (Branch zv zw zx zy zz))
glueVBal1 yv yw yx yy yz zv zw zx zy zz False = glueVBal0 yv yw yx yy yz zv zw zx zy zz otherwise
glueVBal2 yv yw yx yy yz zv zw zx zy zz True = mkBalBranch zv zw (glueVBal (Branch yv yw yx yy yz) zy) zz
glueVBal2 yv yw yx yy yz zv zw zx zy zz False = glueVBal1 yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * size_r < size_l)
size_l  = sizeFM (Branch yv yw yx yy yz)
size_r  = sizeFM (Branch zv zw zx zy zz)

glueVBal4 fm1 EmptyFM = fm1
glueVBal4 wvv wvw = glueVBal3 wvv wvw

glueVBal5 EmptyFM fm2 = fm2
glueVBal5 wvy wvz = glueVBal4 wvy wvz

The following Function with conditions
mkVBalBranch key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
 | sIZE_RATIO * size_l < size_r
 = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv
 | sIZE_RATIO * size_r < size_l
 = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv))
 | otherwise
 = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
where 
size_l  = sizeFM (Branch vux vuy vuz vvu vvv)
size_r  = sizeFM (Branch vvx vvy vvz vwu vwv)

is transformed to
mkVBalBranch key elt EmptyFM fm_r = mkVBalBranch5 key elt EmptyFM fm_r
mkVBalBranch key elt fm_l EmptyFM = mkVBalBranch4 key elt fm_l EmptyFM
mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)

mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = 
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_l < size_r)
where 
mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv))
mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_r < size_l)
size_l  = sizeFM (Branch vux vuy vuz vvu vvv)
size_r  = sizeFM (Branch vvx vvy vvz vwu vwv)

mkVBalBranch4 key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch4 wwx wwy wwz wxu = mkVBalBranch3 wwx wwy wwz wxu

mkVBalBranch5 key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch5 wxw wxx wxy wxz = mkVBalBranch4 wxw wxx wxy wxz

The following Function with conditions
mkBalBranch1 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)
 | sizeFM fm_lr < 2 * sizeFM fm_ll
 = single_R fm_L fm_R
 | otherwise
 = double_R fm_L fm_R

is transformed to
mkBalBranch1 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)

mkBalBranch10 fm_L fm_R vwx vwy vwz fm_ll fm_lr True = double_R fm_L fm_R

mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr True = single_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vwx vwy vwz fm_ll fm_lr otherwise

mkBalBranch12 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

The following Function with conditions
mkBalBranch0 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)
 | sizeFM fm_rl < 2 * sizeFM fm_rr
 = single_L fm_L fm_R
 | otherwise
 = double_L fm_L fm_R

is transformed to
mkBalBranch0 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)

mkBalBranch00 fm_L fm_R vxy vxz vyu fm_rl fm_rr True = double_L fm_L fm_R

mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr True = single_L fm_L fm_R
mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vxy vxz vyu fm_rl fm_rr otherwise

mkBalBranch02 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

The following Function with conditions
mkBalBranch key elt fm_L fm_R
 | size_l + size_r < 2
 = mkBranch 1 key elt fm_L fm_R
 | size_r > sIZE_RATIO * size_l
 = mkBalBranch0 fm_L fm_R fm_R
 | size_l > sIZE_RATIO * size_r
 = mkBalBranch1 fm_L fm_R fm_L
 | otherwise
 = mkBranch 2 key elt fm_L fm_R
where 
double_L fm_l (Branch key_r elt_r vxw (Branch key_rl elt_rl vxx fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vxu fm_ll (Branch key_lr elt_lr vxv fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)
 | sizeFM fm_rl < 2 * sizeFM fm_rr
 = single_L fm_L fm_R
 | otherwise
 = double_L fm_L fm_R
mkBalBranch1 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)
 | sizeFM fm_lr < 2 * sizeFM fm_ll
 = single_R fm_L fm_R
 | otherwise
 = double_R fm_L fm_R
single_L fm_l (Branch key_r elt_r vyv fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vww fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l  = sizeFM fm_L
size_r  = sizeFM fm_R

is transformed to
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

mkBalBranch6 key elt fm_L fm_R = 
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2)
where 
double_L fm_l (Branch key_r elt_r vxw (Branch key_rl elt_rl vxx fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vxu fm_ll (Branch key_lr elt_lr vxv fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vxy vxz vyu fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr True = single_L fm_L fm_R
mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vxy vxz vyu fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vwx vwy vwz fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr True = single_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vwx vwy vwz fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L
mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R
mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vyv fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vww fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l  = sizeFM fm_L
size_r  = sizeFM fm_R

The following Function with conditions
glueBal EmptyFM fm2 = fm2
glueBal fm1 EmptyFM = fm1
glueBal fm1 fm2
 | sizeFM fm2 > sizeFM fm1
 = mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2)
 | otherwise
 = mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2
where 
mid_elt1  = mid_elt10 vv2
mid_elt10 (vyw,mid_elt1) = mid_elt1
mid_elt2  = mid_elt20 vv3
mid_elt20 (vyx,mid_elt2) = mid_elt2
mid_key1  = mid_key10 vv2
mid_key10 (mid_key1,vyy) = mid_key1
mid_key2  = mid_key20 vv3
mid_key20 (mid_key2,vyz) = mid_key2
vv2  = findMax fm1
vv3  = findMin fm2

is transformed to
glueBal EmptyFM fm2 = glueBal4 EmptyFM fm2
glueBal fm1 EmptyFM = glueBal3 fm1 EmptyFM
glueBal fm1 fm2 = glueBal2 fm1 fm2

glueBal2 fm1 fm2 = 
glueBal1 fm1 fm2 (sizeFM fm2 > sizeFM fm1)
where 
glueBal0 fm1 fm2 True = mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2
glueBal1 fm1 fm2 True = mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2)
glueBal1 fm1 fm2 False = glueBal0 fm1 fm2 otherwise
mid_elt1  = mid_elt10 vv2
mid_elt10 (vyw,mid_elt1) = mid_elt1
mid_elt2  = mid_elt20 vv3
mid_elt20 (vyx,mid_elt2) = mid_elt2
mid_key1  = mid_key10 vv2
mid_key10 (mid_key1,vyy) = mid_key1
mid_key2  = mid_key20 vv3
mid_key20 (mid_key2,vyz) = mid_key2
vv2  = findMax fm1
vv3  = findMin fm2

glueBal3 fm1 EmptyFM = fm1
glueBal3 wyx wyy = glueBal2 wyx wyy

glueBal4 EmptyFM fm2 = fm2
glueBal4 wzu wzv = glueBal3 wzu wzv

The following Function with conditions
addToFM_C combiner EmptyFM key elt = unitFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt
 | new_key < key
 = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
 | new_key > key
 = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
 | otherwise
 = Branch new_key (combiner elt new_elt) size fm_l fm_r

is transformed to
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

addToFM_C4 combiner EmptyFM key elt = unitFM key elt
addToFM_C4 wzy wzz xuu xuv = addToFM_C3 wzy wzz xuu xuv

The following Function with conditions
filterFM p EmptyFM = emptyFM
filterFM p (Branch key elt wuu fm_l fm_r)
 | p key elt
 = mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
 | otherwise
 = glueVBal (filterFM p fm_l) (filterFM p fm_r)

is transformed to
filterFM p EmptyFM = filterFM3 p EmptyFM
filterFM p (Branch key elt wuu fm_l fm_r) = filterFM2 p (Branch key elt wuu fm_l fm_r)

filterFM0 p key elt wuu fm_l fm_r True = glueVBal (filterFM p fm_l) (filterFM p fm_r)

filterFM1 p key elt wuu fm_l fm_r True = mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
filterFM1 p key elt wuu fm_l fm_r False = filterFM0 p key elt wuu fm_l fm_r otherwise

filterFM2 p (Branch key elt wuu fm_l fm_r) = filterFM1 p key elt wuu fm_l fm_r (p key elt)

filterFM3 p EmptyFM = emptyFM
filterFM3 xuy xuz = filterFM2 xuy xuz

The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed

mainModule FiniteMap
  ((filterFM :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a) :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap b a = EmptyFM  | Branch b a Int (FiniteMap b a) (FiniteMap b a) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord b => (a  ->  a  ->  a)  ->  FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

  
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

  
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

  
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

  
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

  
addToFM_C4 combiner EmptyFM key elt = unitFM key elt
addToFM_C4 wzy wzz xuu xuv = addToFM_C3 wzy wzz xuu xuv

  deleteMax :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMax (Branch key elt vuu fm_l EmptyFM) = fm_l
deleteMax (Branch key elt vuv fm_l fm_r) = mkBalBranch key elt fm_l (deleteMax fm_r)

  deleteMin :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMin (Branch key elt vzy EmptyFM fm_r) = fm_r
deleteMin (Branch key elt vzz fm_l fm_r) = mkBalBranch key elt (deleteMin fm_l) fm_r

  emptyFM :: FiniteMap a b
emptyFM = EmptyFM

  filterFM :: Ord b => (b  ->  a  ->  Bool)  ->  FiniteMap b a  ->  FiniteMap b a
filterFM p EmptyFM = filterFM3 p EmptyFM
filterFM p (Branch key elt wuu fm_l fm_r) = filterFM2 p (Branch key elt wuu fm_l fm_r)

  
filterFM0 p key elt wuu fm_l fm_r True = glueVBal (filterFM p fm_l) (filterFM p fm_r)

  
filterFM1 p key elt wuu fm_l fm_r True = mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
filterFM1 p key elt wuu fm_l fm_r False = filterFM0 p key elt wuu fm_l fm_r otherwise

  
filterFM2 p (Branch key elt wuu fm_l fm_r) = filterFM1 p key elt wuu fm_l fm_r (p key elt)

  
filterFM3 p EmptyFM = emptyFM
filterFM3 xuy xuz = filterFM2 xuy xuz

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt vzu vzv EmptyFM) = (key,elt)
findMax (Branch key elt vzw vzx fm_r) = findMax fm_r

  findMin :: FiniteMap a b  ->  (a,b)
findMin (Branch key elt wy EmptyFM wz) = (key,elt)
findMin (Branch key elt xu fm_l xv) = findMin fm_l

  glueBal :: Ord b => FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
glueBal EmptyFM fm2 = glueBal4 EmptyFM fm2
glueBal fm1 EmptyFM = glueBal3 fm1 EmptyFM
glueBal fm1 fm2 = glueBal2 fm1 fm2

  
glueBal2 fm1 fm2 = 
glueBal1 fm1 fm2 (sizeFM fm2 > sizeFM fm1) where 
glueBal0 fm1 fm2 True = mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2
glueBal1 fm1 fm2 True = mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2)
glueBal1 fm1 fm2 False = glueBal0 fm1 fm2 otherwise
mid_elt1 = mid_elt10 vv2
mid_elt10 (vyw,mid_elt1) = mid_elt1
mid_elt2 = mid_elt20 vv3
mid_elt20 (vyx,mid_elt2) = mid_elt2
mid_key1 = mid_key10 vv2
mid_key10 (mid_key1,vyy) = mid_key1
mid_key2 = mid_key20 vv3
mid_key20 (mid_key2,vyz) = mid_key2
vv2 = findMax fm1
vv3 = findMin fm2

  
glueBal3 fm1 EmptyFM = fm1
glueBal3 wyx wyy = glueBal2 wyx wyy

  
glueBal4 EmptyFM fm2 = fm2
glueBal4 wzu wzv = glueBal3 wzu wzv

  glueVBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueVBal EmptyFM fm2 = glueVBal5 EmptyFM fm2
glueVBal fm1 EmptyFM = glueVBal4 fm1 EmptyFM
glueVBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) = glueVBal3 (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)

  
glueVBal3 (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) = 
glueVBal2 yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * size_l < size_r) where 
glueVBal0 yv yw yx yy yz zv zw zx zy zz True = glueBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)
glueVBal1 yv yw yx yy yz zv zw zx zy zz True = mkBalBranch yv yw yy (glueVBal yz (Branch zv zw zx zy zz))
glueVBal1 yv yw yx yy yz zv zw zx zy zz False = glueVBal0 yv yw yx yy yz zv zw zx zy zz otherwise
glueVBal2 yv yw yx yy yz zv zw zx zy zz True = mkBalBranch zv zw (glueVBal (Branch yv yw yx yy yz) zy) zz
glueVBal2 yv yw yx yy yz zv zw zx zy zz False = glueVBal1 yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch yv yw yx yy yz)
size_r = sizeFM (Branch zv zw zx zy zz)

  
glueVBal4 fm1 EmptyFM = fm1
glueVBal4 wvv wvw = glueVBal3 wvv wvw

  
glueVBal5 EmptyFM fm2 = fm2
glueVBal5 wvy wvz = glueVBal4 wvy wvz

  mkBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

  
mkBalBranch6 key elt fm_L fm_R = 
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2) where 
double_L fm_l (Branch key_r elt_r vxw (Branch key_rl elt_rl vxx fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vxu fm_ll (Branch key_lr elt_lr vxv fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vxy vxz vyu fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr True = single_L fm_L fm_R
mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vxy vxz vyu fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vwx vwy vwz fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr True = single_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vwx vwy vwz fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L
mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R
mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vyv fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vww fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l = sizeFM fm_L
size_r = sizeFM fm_R

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = 
let 
result = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
 where 
balance_ok = True
left_ok = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key wu wv ww wx) = 
let 
biggest_left_key = fst (findMax fm_l)
in biggest_left_key < key
left_size = sizeFM fm_l
right_ok = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key vw vx vy vz) = 
let 
smallest_right_key = fst (findMin fm_r)
in key < smallest_right_key
right_size = sizeFM fm_r
unbox :: Int  ->  Int
unbox x = x

  mkVBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkVBalBranch key elt EmptyFM fm_r = mkVBalBranch5 key elt EmptyFM fm_r
mkVBalBranch key elt fm_l EmptyFM = mkVBalBranch4 key elt fm_l EmptyFM
mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)

  
mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = 
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_l < size_r) where 
mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv))
mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_r < size_l)
size_l = sizeFM (Branch vux vuy vuz vvu vvv)
size_r = sizeFM (Branch vvx vvy vvz vwu vwv)

  
mkVBalBranch4 key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch4 wwx wwy wwz wxu = mkVBalBranch3 wwx wwy wwz wxu

  
mkVBalBranch5 key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch5 wxw wxx wxy wxz = mkVBalBranch4 wxw wxx wxy wxz

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch xw xx size xy xz) = size

  unitFM :: b  ->  a  ->  FiniteMap b a
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Let/Where Reductions:
The bindings of the following Let/Where expression
mkBalBranch5 key elt fm_L fm_R (size_l + size_r < 2)
where 
double_L fm_l (Branch key_r elt_r vxw (Branch key_rl elt_rl vxx fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 key elt fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)
double_R (Branch key_l elt_l vxu fm_ll (Branch key_lr elt_lr vxv fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 key elt fm_lrr fm_r)
mkBalBranch0 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch02 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)
mkBalBranch00 fm_L fm_R vxy vxz vyu fm_rl fm_rr True = double_L fm_L fm_R
mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr True = single_L fm_L fm_R
mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr False = mkBalBranch00 fm_L fm_R vxy vxz vyu fm_rl fm_rr otherwise
mkBalBranch02 fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch01 fm_L fm_R vxy vxz vyu fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)
mkBalBranch1 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch12 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)
mkBalBranch10 fm_L fm_R vwx vwy vwz fm_ll fm_lr True = double_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr True = single_R fm_L fm_R
mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr False = mkBalBranch10 fm_L fm_R vwx vwy vwz fm_ll fm_lr otherwise
mkBalBranch12 fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch11 fm_L fm_R vwx vwy vwz fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)
mkBalBranch2 key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R
mkBalBranch3 key elt fm_L fm_R True = mkBalBranch1 fm_L fm_R fm_L
mkBalBranch3 key elt fm_L fm_R False = mkBalBranch2 key elt fm_L fm_R otherwise
mkBalBranch4 key elt fm_L fm_R True = mkBalBranch0 fm_L fm_R fm_R
mkBalBranch4 key elt fm_L fm_R False = mkBalBranch3 key elt fm_L fm_R (size_l > sIZE_RATIO * size_r)
mkBalBranch5 key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch5 key elt fm_L fm_R False = mkBalBranch4 key elt fm_L fm_R (size_r > sIZE_RATIO * size_l)
single_L fm_l (Branch key_r elt_r vyv fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 key elt fm_l fm_rl) fm_rr
single_R (Branch key_l elt_l vww fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 key elt fm_lr fm_r)
size_l  = sizeFM fm_L
size_r  = sizeFM fm_R

are unpacked to the following functions on top level
mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 xvu xvv xvw xvx fm_L fm_R fm_R
mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R (mkBalBranch6Size_l xvu xvv xvw xvx > sIZE_RATIO * mkBalBranch6Size_r xvu xvv xvw xvx)

mkBalBranch6Single_R xvu xvv xvw xvx (Branch key_l elt_l vww fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 xvu xvv fm_lr fm_r)

mkBalBranch6Double_R xvu xvv xvw xvx (Branch key_l elt_l vxu fm_ll (Branch key_lr elt_lr vxv fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 xvu xvv fm_lrr fm_r)

mkBalBranch6MkBalBranch1 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch6MkBalBranch12 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)

mkBalBranch6MkBalBranch12 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

mkBalBranch6MkBalBranch10 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr True = mkBalBranch6Double_R xvu xvv xvw xvx fm_L fm_R

mkBalBranch6Single_L xvu xvv xvw xvx fm_l (Branch key_r elt_r vyv fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 xvu xvv fm_l fm_rl) fm_rr

mkBalBranch6MkBalBranch0 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch6MkBalBranch02 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)

mkBalBranch6Double_L xvu xvv xvw xvx fm_l (Branch key_r elt_r vxw (Branch key_rl elt_rl vxx fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 xvu xvv fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

mkBalBranch6MkBalBranch00 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr True = mkBalBranch6Double_L xvu xvv xvw xvx fm_L fm_R

mkBalBranch6MkBalBranch02 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr True = mkBalBranch6Single_L xvu xvv xvw xvx fm_L fm_R
mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr False = mkBalBranch6MkBalBranch00 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr otherwise

mkBalBranch6MkBalBranch2 xvu xvv xvw xvx key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R

mkBalBranch6Size_r xvu xvv xvw xvx = sizeFM xvw

mkBalBranch6Size_l xvu xvv xvw xvx = sizeFM xvx

mkBalBranch6MkBalBranch5 xvu xvv xvw xvx key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch6MkBalBranch5 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R (mkBalBranch6Size_r xvu xvv xvw xvx > sIZE_RATIO * mkBalBranch6Size_l xvu xvv xvw xvx)

mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr True = mkBalBranch6Single_R xvu xvv xvw xvx fm_L fm_R
mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr False = mkBalBranch6MkBalBranch10 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr otherwise

mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 xvu xvv xvw xvx fm_L fm_R fm_L
mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 xvu xvv xvw xvx key elt fm_L fm_R otherwise

The bindings of the following Let/Where expression
glueVBal2 yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * size_l < size_r)
where 
glueVBal0 yv yw yx yy yz zv zw zx zy zz True = glueBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)
glueVBal1 yv yw yx yy yz zv zw zx zy zz True = mkBalBranch yv yw yy (glueVBal yz (Branch zv zw zx zy zz))
glueVBal1 yv yw yx yy yz zv zw zx zy zz False = glueVBal0 yv yw yx yy yz zv zw zx zy zz otherwise
glueVBal2 yv yw yx yy yz zv zw zx zy zz True = mkBalBranch zv zw (glueVBal (Branch yv yw yx yy yz) zy) zz
glueVBal2 yv yw yx yy yz zv zw zx zy zz False = glueVBal1 yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * size_r < size_l)
size_l  = sizeFM (Branch yv yw yx yy yz)
size_r  = sizeFM (Branch zv zw zx zy zz)

are unpacked to the following functions on top level
glueVBal3Size_r xvy xvz xwu xwv xww xwx xwy xwz xxu xxv = sizeFM (Branch xvy xvz xwu xwv xww)

glueVBal3GlueVBal0 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = glueBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)

glueVBal3Size_l xvy xvz xwu xwv xww xwx xwy xwz xxu xxv = sizeFM (Branch xwx xwy xwz xxu xxv)

glueVBal3GlueVBal2 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = mkBalBranch zv zw (glueVBal (Branch yv yw yx yy yz) zy) zz
glueVBal3GlueVBal2 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz False = glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * glueVBal3Size_r xvy xvz xwu xwv xww xwx xwy xwz xxu xxv < glueVBal3Size_l xvy xvz xwu xwv xww xwx xwy xwz xxu xxv)

glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = mkBalBranch yv yw yy (glueVBal yz (Branch zv zw zx zy zz))
glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz False = glueVBal3GlueVBal0 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz otherwise

The bindings of the following Let/Where expression
let 
result  = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result
where 
balance_ok  = True
left_ok  = left_ok0 fm_l key fm_l
left_ok0 fm_l key EmptyFM = True
left_ok0 fm_l key (Branch left_key wu wv ww wx) = 
let 
biggest_left_key  = fst (findMax fm_l)
in biggest_left_key < key
left_size  = sizeFM fm_l
right_ok  = right_ok0 fm_r key fm_r
right_ok0 fm_r key EmptyFM = True
right_ok0 fm_r key (Branch right_key vw vx vy vz) = 
let 
smallest_right_key  = fst (findMin fm_r)
in key < smallest_right_key
right_size  = sizeFM fm_r
unbox x = x

are unpacked to the following functions on top level
mkBranchBalance_ok xxw xxx xxy = True

mkBranchLeft_ok xxw xxx xxy = mkBranchLeft_ok0 xxw xxx xxy xxw xxx xxw

mkBranchRight_ok xxw xxx xxy = mkBranchRight_ok0 xxw xxx xxy xxy xxx xxy

mkBranchRight_ok0 xxw xxx xxy fm_r key EmptyFM = True
mkBranchRight_ok0 xxw xxx xxy fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r

mkBranchRight_size xxw xxx xxy = sizeFM xxy

mkBranchLeft_size xxw xxx xxy = sizeFM xxw

mkBranchUnbox xxw xxx xxy x = x

mkBranchLeft_ok0 xxw xxx xxy fm_l key EmptyFM = True
mkBranchLeft_ok0 xxw xxx xxy fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key

The bindings of the following Let/Where expression
let 
result  = Branch key elt (unbox (1 + left_size + right_size)) fm_l fm_r
in result

are unpacked to the following functions on top level
mkBranchResult xxz xyu xyv xyw = Branch xxz xyu (mkBranchUnbox xyv xxz xyw (1 + mkBranchLeft_size xyv xxz xyw + mkBranchRight_size xyv xxz xyw)) xyv xyw

The bindings of the following Let/Where expression
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_l < size_r)
where 
mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)
mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv))
mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch0 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv
mkVBalBranch2 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch1 key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * size_r < size_l)
size_l  = sizeFM (Branch vux vuy vuz vvu vvv)
size_r  = sizeFM (Branch vvx vvy vvz vwu vwv)

are unpacked to the following functions on top level
mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv))
mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch3MkVBalBranch0 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise

mkVBalBranch3Size_r xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu = sizeFM (Branch xyx xyy xyz xzu xzv)

mkVBalBranch3MkVBalBranch0 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)

mkVBalBranch3Size_l xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu = sizeFM (Branch xzw xzx xzy xzz yuu)

mkVBalBranch3MkVBalBranch2 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv
mkVBalBranch3MkVBalBranch2 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * mkVBalBranch3Size_r xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu < mkVBalBranch3Size_l xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu)

The bindings of the following Let/Where expression
glueBal1 fm1 fm2 (sizeFM fm2 > sizeFM fm1)
where 
glueBal0 fm1 fm2 True = mkBalBranch mid_key1 mid_elt1 (deleteMax fm1) fm2
glueBal1 fm1 fm2 True = mkBalBranch mid_key2 mid_elt2 fm1 (deleteMin fm2)
glueBal1 fm1 fm2 False = glueBal0 fm1 fm2 otherwise
mid_elt1  = mid_elt10 vv2
mid_elt10 (vyw,mid_elt1) = mid_elt1
mid_elt2  = mid_elt20 vv3
mid_elt20 (vyx,mid_elt2) = mid_elt2
mid_key1  = mid_key10 vv2
mid_key10 (mid_key1,vyy) = mid_key1
mid_key2  = mid_key20 vv3
mid_key20 (mid_key2,vyz) = mid_key2
vv2  = findMax fm1
vv3  = findMin fm2

are unpacked to the following functions on top level
glueBal2Mid_elt1 yuv yuw = glueBal2Mid_elt10 yuv yuw (glueBal2Vv2 yuv yuw)

glueBal2Vv2 yuv yuw = findMax yuv

glueBal2Mid_elt2 yuv yuw = glueBal2Mid_elt20 yuv yuw (glueBal2Vv3 yuv yuw)

glueBal2Vv3 yuv yuw = findMin yuw

glueBal2Mid_elt20 yuv yuw (vyx,mid_elt2) = mid_elt2

glueBal2Mid_key1 yuv yuw = glueBal2Mid_key10 yuv yuw (glueBal2Vv2 yuv yuw)

glueBal2GlueBal1 yuv yuw fm1 fm2 True = mkBalBranch (glueBal2Mid_key2 yuv yuw) (glueBal2Mid_elt2 yuv yuw) fm1 (deleteMin fm2)
glueBal2GlueBal1 yuv yuw fm1 fm2 False = glueBal2GlueBal0 yuv yuw fm1 fm2 otherwise

glueBal2Mid_key10 yuv yuw (mid_key1,vyy) = mid_key1

glueBal2GlueBal0 yuv yuw fm1 fm2 True = mkBalBranch (glueBal2Mid_key1 yuv yuw) (glueBal2Mid_elt1 yuv yuw) (deleteMax fm1) fm2

glueBal2Mid_key20 yuv yuw (mid_key2,vyz) = mid_key2

glueBal2Mid_key2 yuv yuw = glueBal2Mid_key20 yuv yuw (glueBal2Vv3 yuv yuw)

glueBal2Mid_elt10 yuv yuw (vyw,mid_elt1) = mid_elt1

The bindings of the following Let/Where expression
let 
smallest_right_key  = fst (findMin fm_r)
in key < smallest_right_key

are unpacked to the following functions on top level
mkBranchRight_ok0Smallest_right_key yux = fst (findMin yux)

The bindings of the following Let/Where expression
let 
biggest_left_key  = fst (findMax fm_l)
in biggest_left_key < key

are unpacked to the following functions on top level
mkBranchLeft_ok0Biggest_left_key yuy = fst (findMax yuy)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed

mainModule FiniteMap
  ((filterFM :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a) :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap a b) where 
  addToFM :: Ord a => FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord a => (b  ->  b  ->  b)  ->  FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

  
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

  
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

  
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

  
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

  
addToFM_C4 combiner EmptyFM key elt = unitFM key elt
addToFM_C4 wzy wzz xuu xuv = addToFM_C3 wzy wzz xuu xuv

  deleteMax :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMax (Branch key elt vuu fm_l EmptyFM) = fm_l
deleteMax (Branch key elt vuv fm_l fm_r) = mkBalBranch key elt fm_l (deleteMax fm_r)

  deleteMin :: Ord b => FiniteMap b a  ->  FiniteMap b a
deleteMin (Branch key elt vzy EmptyFM fm_r) = fm_r
deleteMin (Branch key elt vzz fm_l fm_r) = mkBalBranch key elt (deleteMin fm_l) fm_r

  emptyFM :: FiniteMap b a
emptyFM = EmptyFM

  filterFM :: Ord a => (a  ->  b  ->  Bool)  ->  FiniteMap a b  ->  FiniteMap a b
filterFM p EmptyFM = filterFM3 p EmptyFM
filterFM p (Branch key elt wuu fm_l fm_r) = filterFM2 p (Branch key elt wuu fm_l fm_r)

  
filterFM0 p key elt wuu fm_l fm_r True = glueVBal (filterFM p fm_l) (filterFM p fm_r)

  
filterFM1 p key elt wuu fm_l fm_r True = mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
filterFM1 p key elt wuu fm_l fm_r False = filterFM0 p key elt wuu fm_l fm_r otherwise

  
filterFM2 p (Branch key elt wuu fm_l fm_r) = filterFM1 p key elt wuu fm_l fm_r (p key elt)

  
filterFM3 p EmptyFM = emptyFM
filterFM3 xuy xuz = filterFM2 xuy xuz

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt vzu vzv EmptyFM) = (key,elt)
findMax (Branch key elt vzw vzx fm_r) = findMax fm_r

  findMin :: FiniteMap a b  ->  (a,b)
findMin (Branch key elt wy EmptyFM wz) = (key,elt)
findMin (Branch key elt xu fm_l xv) = findMin fm_l

  glueBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueBal EmptyFM fm2 = glueBal4 EmptyFM fm2
glueBal fm1 EmptyFM = glueBal3 fm1 EmptyFM
glueBal fm1 fm2 = glueBal2 fm1 fm2

  
glueBal2 fm1 fm2 = glueBal2GlueBal1 fm1 fm2 fm1 fm2 (sizeFM fm2 > sizeFM fm1)

  
glueBal2GlueBal0 yuv yuw fm1 fm2 True = mkBalBranch (glueBal2Mid_key1 yuv yuw) (glueBal2Mid_elt1 yuv yuw) (deleteMax fm1) fm2

  
glueBal2GlueBal1 yuv yuw fm1 fm2 True = mkBalBranch (glueBal2Mid_key2 yuv yuw) (glueBal2Mid_elt2 yuv yuw) fm1 (deleteMin fm2)
glueBal2GlueBal1 yuv yuw fm1 fm2 False = glueBal2GlueBal0 yuv yuw fm1 fm2 otherwise

  
glueBal2Mid_elt1 yuv yuw = glueBal2Mid_elt10 yuv yuw (glueBal2Vv2 yuv yuw)

  
glueBal2Mid_elt10 yuv yuw (vyw,mid_elt1) = mid_elt1

  
glueBal2Mid_elt2 yuv yuw = glueBal2Mid_elt20 yuv yuw (glueBal2Vv3 yuv yuw)

  
glueBal2Mid_elt20 yuv yuw (vyx,mid_elt2) = mid_elt2

  
glueBal2Mid_key1 yuv yuw = glueBal2Mid_key10 yuv yuw (glueBal2Vv2 yuv yuw)

  
glueBal2Mid_key10 yuv yuw (mid_key1,vyy) = mid_key1

  
glueBal2Mid_key2 yuv yuw = glueBal2Mid_key20 yuv yuw (glueBal2Vv3 yuv yuw)

  
glueBal2Mid_key20 yuv yuw (mid_key2,vyz) = mid_key2

  
glueBal2Vv2 yuv yuw = findMax yuv

  
glueBal2Vv3 yuv yuw = findMin yuw

  
glueBal3 fm1 EmptyFM = fm1
glueBal3 wyx wyy = glueBal2 wyx wyy

  
glueBal4 EmptyFM fm2 = fm2
glueBal4 wzu wzv = glueBal3 wzu wzv

  glueVBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueVBal EmptyFM fm2 = glueVBal5 EmptyFM fm2
glueVBal fm1 EmptyFM = glueVBal4 fm1 EmptyFM
glueVBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) = glueVBal3 (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)

  
glueVBal3 (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) = glueVBal3GlueVBal2 zv zw zx zy zz yv yw yx yy yz yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * glueVBal3Size_l zv zw zx zy zz yv yw yx yy yz < glueVBal3Size_r zv zw zx zy zz yv yw yx yy yz)

  
glueVBal3GlueVBal0 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = glueBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)

  
glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = mkBalBranch yv yw yy (glueVBal yz (Branch zv zw zx zy zz))
glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz False = glueVBal3GlueVBal0 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz otherwise

  
glueVBal3GlueVBal2 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = mkBalBranch zv zw (glueVBal (Branch yv yw yx yy yz) zy) zz
glueVBal3GlueVBal2 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz False = glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * glueVBal3Size_r xvy xvz xwu xwv xww xwx xwy xwz xxu xxv < glueVBal3Size_l xvy xvz xwu xwv xww xwx xwy xwz xxu xxv)

  
glueVBal3Size_l xvy xvz xwu xwv xww xwx xwy xwz xxu xxv = sizeFM (Branch xwx xwy xwz xxu xxv)

  
glueVBal3Size_r xvy xvz xwu xwv xww xwx xwy xwz xxu xxv = sizeFM (Branch xvy xvz xwu xwv xww)

  
glueVBal4 fm1 EmptyFM = fm1
glueVBal4 wvv wvw = glueVBal3 wvv wvw

  
glueVBal5 EmptyFM fm2 = fm2
glueVBal5 wvy wvz = glueVBal4 wvy wvz

  mkBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

  
mkBalBranch6 key elt fm_L fm_R = mkBalBranch6MkBalBranch5 key elt fm_R fm_L key elt fm_L fm_R (mkBalBranch6Size_l key elt fm_R fm_L + mkBalBranch6Size_r key elt fm_R fm_L < 2)

  
mkBalBranch6Double_L xvu xvv xvw xvx fm_l (Branch key_r elt_r vxw (Branch key_rl elt_rl vxx fm_rll fm_rlr) fm_rr) = mkBranch 5 key_rl elt_rl (mkBranch 6 xvu xvv fm_l fm_rll) (mkBranch 7 key_r elt_r fm_rlr fm_rr)

  
mkBalBranch6Double_R xvu xvv xvw xvx (Branch key_l elt_l vxu fm_ll (Branch key_lr elt_lr vxv fm_lrl fm_lrr)) fm_r = mkBranch 10 key_lr elt_lr (mkBranch 11 key_l elt_l fm_ll fm_lrl) (mkBranch 12 xvu xvv fm_lrr fm_r)

  
mkBalBranch6MkBalBranch0 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch6MkBalBranch02 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)

  
mkBalBranch6MkBalBranch00 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr True = mkBalBranch6Double_L xvu xvv xvw xvx fm_L fm_R

  
mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr True = mkBalBranch6Single_L xvu xvv xvw xvx fm_L fm_R
mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr False = mkBalBranch6MkBalBranch00 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr otherwise

  
mkBalBranch6MkBalBranch02 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr (sizeFM fm_rl < 2 * sizeFM fm_rr)

  
mkBalBranch6MkBalBranch1 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch6MkBalBranch12 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)

  
mkBalBranch6MkBalBranch10 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr True = mkBalBranch6Double_R xvu xvv xvw xvx fm_L fm_R

  
mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr True = mkBalBranch6Single_R xvu xvv xvw xvx fm_L fm_R
mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr False = mkBalBranch6MkBalBranch10 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr otherwise

  
mkBalBranch6MkBalBranch12 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr (sizeFM fm_lr < 2 * sizeFM fm_ll)

  
mkBalBranch6MkBalBranch2 xvu xvv xvw xvx key elt fm_L fm_R True = mkBranch 2 key elt fm_L fm_R

  
mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 xvu xvv xvw xvx fm_L fm_R fm_L
mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 xvu xvv xvw xvx key elt fm_L fm_R otherwise

  
mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 xvu xvv xvw xvx fm_L fm_R fm_R
mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R (mkBalBranch6Size_l xvu xvv xvw xvx > sIZE_RATIO * mkBalBranch6Size_r xvu xvv xvw xvx)

  
mkBalBranch6MkBalBranch5 xvu xvv xvw xvx key elt fm_L fm_R True = mkBranch 1 key elt fm_L fm_R
mkBalBranch6MkBalBranch5 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R (mkBalBranch6Size_r xvu xvv xvw xvx > sIZE_RATIO * mkBalBranch6Size_l xvu xvv xvw xvx)

  
mkBalBranch6Single_L xvu xvv xvw xvx fm_l (Branch key_r elt_r vyv fm_rl fm_rr) = mkBranch 3 key_r elt_r (mkBranch 4 xvu xvv fm_l fm_rl) fm_rr

  
mkBalBranch6Single_R xvu xvv xvw xvx (Branch key_l elt_l vww fm_ll fm_lr) fm_r = mkBranch 8 key_l elt_l fm_ll (mkBranch 9 xvu xvv fm_lr fm_r)

  
mkBalBranch6Size_l xvu xvv xvw xvx = sizeFM xvx

  
mkBalBranch6Size_r xvu xvv xvw xvx = sizeFM xvw

  mkBranch :: Ord a => Int  ->  a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkBranch which key elt fm_l fm_r = mkBranchResult key elt fm_l fm_r

  
mkBranchBalance_ok xxw xxx xxy = True

  
mkBranchLeft_ok xxw xxx xxy = mkBranchLeft_ok0 xxw xxx xxy xxw xxx xxw

  
mkBranchLeft_ok0 xxw xxx xxy fm_l key EmptyFM = True
mkBranchLeft_ok0 xxw xxx xxy fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key

  
mkBranchLeft_ok0Biggest_left_key yuy = fst (findMax yuy)

  
mkBranchLeft_size xxw xxx xxy = sizeFM xxw

  
mkBranchResult xxz xyu xyv xyw = Branch xxz xyu (mkBranchUnbox xyv xxz xyw (1 + mkBranchLeft_size xyv xxz xyw + mkBranchRight_size xyv xxz xyw)) xyv xyw

  
mkBranchRight_ok xxw xxx xxy = mkBranchRight_ok0 xxw xxx xxy xxy xxx xxy

  
mkBranchRight_ok0 xxw xxx xxy fm_r key EmptyFM = True
mkBranchRight_ok0 xxw xxx xxy fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r

  
mkBranchRight_ok0Smallest_right_key yux = fst (findMin yux)

  
mkBranchRight_size xxw xxx xxy = sizeFM xxy

  mkBranchUnbox :: Ord a =>  ->  (FiniteMap a b) ( ->  a ( ->  (FiniteMap a b) (Int  ->  Int)))
mkBranchUnbox xxw xxx xxy x = x

  mkVBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkVBalBranch key elt EmptyFM fm_r = mkVBalBranch5 key elt EmptyFM fm_r
mkVBalBranch key elt fm_l EmptyFM = mkVBalBranch4 key elt fm_l EmptyFM
mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)

  
mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = mkVBalBranch3MkVBalBranch2 vvx vvy vvz vwu vwv vux vuy vuz vvu vvv key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * mkVBalBranch3Size_l vvx vvy vvz vwu vwv vux vuy vuz vvu vvv < mkVBalBranch3Size_r vvx vvy vvz vwu vwv vux vuy vuz vvu vvv)

  
mkVBalBranch3MkVBalBranch0 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch 13 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)

  
mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv))
mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch3MkVBalBranch0 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise

  
mkVBalBranch3MkVBalBranch2 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv
mkVBalBranch3MkVBalBranch2 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * mkVBalBranch3Size_r xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu < mkVBalBranch3Size_l xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu)

  
mkVBalBranch3Size_l xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu = sizeFM (Branch xzw xzx xzy xzz yuu)

  
mkVBalBranch3Size_r xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu = sizeFM (Branch xyx xyy xyz xzu xzv)

  
mkVBalBranch4 key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch4 wwx wwy wwz wxu = mkVBalBranch3 wwx wwy wwz wxu

  
mkVBalBranch5 key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch5 wxw wxx wxy wxz = mkVBalBranch4 wxw wxx wxy wxz

  sIZE_RATIO :: Int
sIZE_RATIO = 5

  sizeFM :: FiniteMap a b  ->  Int
sizeFM EmptyFM = 0
sizeFM (Branch xw xx size xy xz) = size

  unitFM :: b  ->  a  ->  FiniteMap b a
unitFM key elt = Branch key elt 1 emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow

mainModule FiniteMap
  (filterFM :: (Float  ->  a  ->  Bool)  ->  FiniteMap Float a  ->  FiniteMap Float a)

module FiniteMap where
  import qualified Maybe
import qualified Prelude
  data FiniteMap a b = EmptyFM  | Branch a b Int (FiniteMap a b) (FiniteMap a b) 
  instance (Eq a, Eq b) => Eq (FiniteMap b a) where 
  addToFM :: Ord b => FiniteMap b a  ->  b  ->  a  ->  FiniteMap b a
addToFM fm key elt = addToFM_C addToFM0 fm key elt

  
addToFM0 old new = new

  addToFM_C :: Ord a => (b  ->  b  ->  b)  ->  FiniteMap a b  ->  a  ->  b  ->  FiniteMap a b
addToFM_C combiner EmptyFM key elt = addToFM_C4 combiner EmptyFM key elt
addToFM_C combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt

  
addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt True = Branch new_key (combiner elt new_elt) size fm_l fm_r

  
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt fm_l (addToFM_C combiner fm_r new_key new_elt)
addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C0 combiner key elt size fm_l fm_r new_key new_elt otherwise

  
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt True = mkBalBranch key elt (addToFM_C combiner fm_l new_key new_elt) fm_r
addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt False = addToFM_C1 combiner key elt size fm_l fm_r new_key new_elt (new_key > key)

  
addToFM_C3 combiner (Branch key elt size fm_l fm_r) new_key new_elt = addToFM_C2 combiner key elt size fm_l fm_r new_key new_elt (new_key < key)

  
addToFM_C4 combiner EmptyFM key elt = unitFM key elt
addToFM_C4 wzy wzz xuu xuv = addToFM_C3 wzy wzz xuu xuv

  deleteMax :: Ord b => FiniteMap b a  ->  FiniteMap b a
deleteMax (Branch key elt vuu fm_l EmptyFM) = fm_l
deleteMax (Branch key elt vuv fm_l fm_r) = mkBalBranch key elt fm_l (deleteMax fm_r)

  deleteMin :: Ord a => FiniteMap a b  ->  FiniteMap a b
deleteMin (Branch key elt vzy EmptyFM fm_r) = fm_r
deleteMin (Branch key elt vzz fm_l fm_r) = mkBalBranch key elt (deleteMin fm_l) fm_r

  emptyFM :: FiniteMap b a
emptyFM = EmptyFM

  filterFM :: Ord a => (a  ->  b  ->  Bool)  ->  FiniteMap a b  ->  FiniteMap a b
filterFM p EmptyFM = filterFM3 p EmptyFM
filterFM p (Branch key elt wuu fm_l fm_r) = filterFM2 p (Branch key elt wuu fm_l fm_r)

  
filterFM0 p key elt wuu fm_l fm_r True = glueVBal (filterFM p fm_l) (filterFM p fm_r)

  
filterFM1 p key elt wuu fm_l fm_r True = mkVBalBranch key elt (filterFM p fm_l) (filterFM p fm_r)
filterFM1 p key elt wuu fm_l fm_r False = filterFM0 p key elt wuu fm_l fm_r otherwise

  
filterFM2 p (Branch key elt wuu fm_l fm_r) = filterFM1 p key elt wuu fm_l fm_r (p key elt)

  
filterFM3 p EmptyFM = emptyFM
filterFM3 xuy xuz = filterFM2 xuy xuz

  findMax :: FiniteMap b a  ->  (b,a)
findMax (Branch key elt vzu vzv EmptyFM) = (key,elt)
findMax (Branch key elt vzw vzx fm_r) = findMax fm_r

  findMin :: FiniteMap a b  ->  (a,b)
findMin (Branch key elt wy EmptyFM wz) = (key,elt)
findMin (Branch key elt xu fm_l xv) = findMin fm_l

  glueBal :: Ord b => FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
glueBal EmptyFM fm2 = glueBal4 EmptyFM fm2
glueBal fm1 EmptyFM = glueBal3 fm1 EmptyFM
glueBal fm1 fm2 = glueBal2 fm1 fm2

  
glueBal2 fm1 fm2 = glueBal2GlueBal1 fm1 fm2 fm1 fm2 (sizeFM fm2 > sizeFM fm1)

  
glueBal2GlueBal0 yuv yuw fm1 fm2 True = mkBalBranch (glueBal2Mid_key1 yuv yuw) (glueBal2Mid_elt1 yuv yuw) (deleteMax fm1) fm2

  
glueBal2GlueBal1 yuv yuw fm1 fm2 True = mkBalBranch (glueBal2Mid_key2 yuv yuw) (glueBal2Mid_elt2 yuv yuw) fm1 (deleteMin fm2)
glueBal2GlueBal1 yuv yuw fm1 fm2 False = glueBal2GlueBal0 yuv yuw fm1 fm2 otherwise

  
glueBal2Mid_elt1 yuv yuw = glueBal2Mid_elt10 yuv yuw (glueBal2Vv2 yuv yuw)

  
glueBal2Mid_elt10 yuv yuw (vyw,mid_elt1) = mid_elt1

  
glueBal2Mid_elt2 yuv yuw = glueBal2Mid_elt20 yuv yuw (glueBal2Vv3 yuv yuw)

  
glueBal2Mid_elt20 yuv yuw (vyx,mid_elt2) = mid_elt2

  
glueBal2Mid_key1 yuv yuw = glueBal2Mid_key10 yuv yuw (glueBal2Vv2 yuv yuw)

  
glueBal2Mid_key10 yuv yuw (mid_key1,vyy) = mid_key1

  
glueBal2Mid_key2 yuv yuw = glueBal2Mid_key20 yuv yuw (glueBal2Vv3 yuv yuw)

  
glueBal2Mid_key20 yuv yuw (mid_key2,vyz) = mid_key2

  
glueBal2Vv2 yuv yuw = findMax yuv

  
glueBal2Vv3 yuv yuw = findMin yuw

  
glueBal3 fm1 EmptyFM = fm1
glueBal3 wyx wyy = glueBal2 wyx wyy

  
glueBal4 EmptyFM fm2 = fm2
glueBal4 wzu wzv = glueBal3 wzu wzv

  glueVBal :: Ord a => FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
glueVBal EmptyFM fm2 = glueVBal5 EmptyFM fm2
glueVBal fm1 EmptyFM = glueVBal4 fm1 EmptyFM
glueVBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) = glueVBal3 (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)

  
glueVBal3 (Branch yv yw yx yy yz) (Branch zv zw zx zy zz) = glueVBal3GlueVBal2 zv zw zx zy zz yv yw yx yy yz yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * glueVBal3Size_l zv zw zx zy zz yv yw yx yy yz < glueVBal3Size_r zv zw zx zy zz yv yw yx yy yz)

  
glueVBal3GlueVBal0 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = glueBal (Branch yv yw yx yy yz) (Branch zv zw zx zy zz)

  
glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = mkBalBranch yv yw yy (glueVBal yz (Branch zv zw zx zy zz))
glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz False = glueVBal3GlueVBal0 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz otherwise

  
glueVBal3GlueVBal2 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz True = mkBalBranch zv zw (glueVBal (Branch yv yw yx yy yz) zy) zz
glueVBal3GlueVBal2 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz False = glueVBal3GlueVBal1 xvy xvz xwu xwv xww xwx xwy xwz xxu xxv yv yw yx yy yz zv zw zx zy zz (sIZE_RATIO * glueVBal3Size_r xvy xvz xwu xwv xww xwx xwy xwz xxu xxv < glueVBal3Size_l xvy xvz xwu xwv xww xwx xwy xwz xxu xxv)

  
glueVBal3Size_l xvy xvz xwu xwv xww xwx xwy xwz xxu xxv = sizeFM (Branch xwx xwy xwz xxu xxv)

  
glueVBal3Size_r xvy xvz xwu xwv xww xwx xwy xwz xxu xxv = sizeFM (Branch xvy xvz xwu xwv xww)

  
glueVBal4 fm1 EmptyFM = fm1
glueVBal4 wvv wvw = glueVBal3 wvv wvw

  
glueVBal5 EmptyFM fm2 = fm2
glueVBal5 wvy wvz = glueVBal4 wvy wvz

  mkBalBranch :: Ord b => b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBalBranch key elt fm_L fm_R = mkBalBranch6 key elt fm_L fm_R

  
mkBalBranch6 key elt fm_L fm_R = mkBalBranch6MkBalBranch5 key elt fm_R fm_L key elt fm_L fm_R (mkBalBranch6Size_l key elt fm_R fm_L + mkBalBranch6Size_r key elt fm_R fm_L < Pos (Succ (Succ Zero)))

  
mkBalBranch6Double_L xvu xvv xvw xvx fm_l (Branch key_r elt_r vxw (Branch key_rl elt_rl vxx fm_rll fm_rlr) fm_rr) = mkBranch (Pos (Succ (Succ (Succ (Succ (Succ Zero)))))) key_rl elt_rl (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))) xvu xvv fm_l fm_rll) (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))) key_r elt_r fm_rlr fm_rr)

  
mkBalBranch6Double_R xvu xvv xvw xvx (Branch key_l elt_l vxu fm_ll (Branch key_lr elt_lr vxv fm_lrl fm_lrr)) fm_r = mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))) key_lr elt_lr (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))) key_l elt_l fm_ll fm_lrl) (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))) xvu xvv fm_lrr fm_r)

  
mkBalBranch6MkBalBranch0 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch6MkBalBranch02 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr)

  
mkBalBranch6MkBalBranch00 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr True = mkBalBranch6Double_L xvu xvv xvw xvx fm_L fm_R

  
mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr True = mkBalBranch6Single_L xvu xvv xvw xvx fm_L fm_R
mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr False = mkBalBranch6MkBalBranch00 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr otherwise

  
mkBalBranch6MkBalBranch02 xvu xvv xvw xvx fm_L fm_R (Branch vxy vxz vyu fm_rl fm_rr) = mkBalBranch6MkBalBranch01 xvu xvv xvw xvx fm_L fm_R vxy vxz vyu fm_rl fm_rr (sizeFM fm_rl < Pos (Succ (Succ Zero)) * sizeFM fm_rr)

  
mkBalBranch6MkBalBranch1 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch6MkBalBranch12 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr)

  
mkBalBranch6MkBalBranch10 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr True = mkBalBranch6Double_R xvu xvv xvw xvx fm_L fm_R

  
mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr True = mkBalBranch6Single_R xvu xvv xvw xvx fm_L fm_R
mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr False = mkBalBranch6MkBalBranch10 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr otherwise

  
mkBalBranch6MkBalBranch12 xvu xvv xvw xvx fm_L fm_R (Branch vwx vwy vwz fm_ll fm_lr) = mkBalBranch6MkBalBranch11 xvu xvv xvw xvx fm_L fm_R vwx vwy vwz fm_ll fm_lr (sizeFM fm_lr < Pos (Succ (Succ Zero)) * sizeFM fm_ll)

  
mkBalBranch6MkBalBranch2 xvu xvv xvw xvx key elt fm_L fm_R True = mkBranch (Pos (Succ (Succ Zero))) key elt fm_L fm_R

  
mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R True = mkBalBranch6MkBalBranch1 xvu xvv xvw xvx fm_L fm_R fm_L
mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch2 xvu xvv xvw xvx key elt fm_L fm_R otherwise

  
mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R True = mkBalBranch6MkBalBranch0 xvu xvv xvw xvx fm_L fm_R fm_R
mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch3 xvu xvv xvw xvx key elt fm_L fm_R (mkBalBranch6Size_l xvu xvv xvw xvx > sIZE_RATIO * mkBalBranch6Size_r xvu xvv xvw xvx)

  
mkBalBranch6MkBalBranch5 xvu xvv xvw xvx key elt fm_L fm_R True = mkBranch (Pos (Succ Zero)) key elt fm_L fm_R
mkBalBranch6MkBalBranch5 xvu xvv xvw xvx key elt fm_L fm_R False = mkBalBranch6MkBalBranch4 xvu xvv xvw xvx key elt fm_L fm_R (mkBalBranch6Size_r xvu xvv xvw xvx > sIZE_RATIO * mkBalBranch6Size_l xvu xvv xvw xvx)

  
mkBalBranch6Single_L xvu xvv xvw xvx fm_l (Branch key_r elt_r vyv fm_rl fm_rr) = mkBranch (Pos (Succ (Succ (Succ Zero)))) key_r elt_r (mkBranch (Pos (Succ (Succ (Succ (Succ Zero))))) xvu xvv fm_l fm_rl) fm_rr

  
mkBalBranch6Single_R xvu xvv xvw xvx (Branch key_l elt_l vww fm_ll fm_lr) fm_r = mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))) key_l elt_l fm_ll (mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))) xvu xvv fm_lr fm_r)

  
mkBalBranch6Size_l xvu xvv xvw xvx = sizeFM xvx

  
mkBalBranch6Size_r xvu xvv xvw xvx = sizeFM xvw

  mkBranch :: Ord b => Int  ->  b  ->  a  ->  FiniteMap b a  ->  FiniteMap b a  ->  FiniteMap b a
mkBranch which key elt fm_l fm_r = mkBranchResult key elt fm_l fm_r

  
mkBranchBalance_ok xxw xxx xxy = True

  
mkBranchLeft_ok xxw xxx xxy = mkBranchLeft_ok0 xxw xxx xxy xxw xxx xxw

  
mkBranchLeft_ok0 xxw xxx xxy fm_l key EmptyFM = True
mkBranchLeft_ok0 xxw xxx xxy fm_l key (Branch left_key wu wv ww wx) = mkBranchLeft_ok0Biggest_left_key fm_l < key

  
mkBranchLeft_ok0Biggest_left_key yuy = fst (findMax yuy)

  
mkBranchLeft_size xxw xxx xxy = sizeFM xxw

  
mkBranchResult xxz xyu xyv xyw = Branch xxz xyu (mkBranchUnbox xyv xxz xyw (Pos (Succ Zero) + mkBranchLeft_size xyv xxz xyw + mkBranchRight_size xyv xxz xyw)) xyv xyw

  
mkBranchRight_ok xxw xxx xxy = mkBranchRight_ok0 xxw xxx xxy xxy xxx xxy

  
mkBranchRight_ok0 xxw xxx xxy fm_r key EmptyFM = True
mkBranchRight_ok0 xxw xxx xxy fm_r key (Branch right_key vw vx vy vz) = key < mkBranchRight_ok0Smallest_right_key fm_r

  
mkBranchRight_ok0Smallest_right_key yux = fst (findMin yux)

  
mkBranchRight_size xxw xxx xxy = sizeFM xxy

  mkBranchUnbox :: Ord a =>  ->  (FiniteMap a b) ( ->  a ( ->  (FiniteMap a b) (Int  ->  Int)))
mkBranchUnbox xxw xxx xxy x = x

  mkVBalBranch :: Ord a => a  ->  b  ->  FiniteMap a b  ->  FiniteMap a b  ->  FiniteMap a b
mkVBalBranch key elt EmptyFM fm_r = mkVBalBranch5 key elt EmptyFM fm_r
mkVBalBranch key elt fm_l EmptyFM = mkVBalBranch4 key elt fm_l EmptyFM
mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)

  
mkVBalBranch3 key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv) = mkVBalBranch3MkVBalBranch2 vvx vvy vvz vwu vwv vux vuy vuz vvu vvv key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * mkVBalBranch3Size_l vvx vvy vvz vwu vwv vux vuy vuz vvu vvv < mkVBalBranch3Size_r vvx vvy vvz vwu vwv vux vuy vuz vvu vvv)

  
mkVBalBranch3MkVBalBranch0 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBranch (Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))) key elt (Branch vux vuy vuz vvu vvv) (Branch vvx vvy vvz vwu vwv)

  
mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vux vuy vvu (mkVBalBranch key elt vvv (Branch vvx vvy vvz vwu vwv))
mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch3MkVBalBranch0 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv otherwise

  
mkVBalBranch3MkVBalBranch2 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv True = mkBalBranch vvx vvy (mkVBalBranch key elt (Branch vux vuy vuz vvu vvv) vwu) vwv
mkVBalBranch3MkVBalBranch2 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv False = mkVBalBranch3MkVBalBranch1 xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu key elt vux vuy vuz vvu vvv vvx vvy vvz vwu vwv (sIZE_RATIO * mkVBalBranch3Size_r xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu < mkVBalBranch3Size_l xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu)

  
mkVBalBranch3Size_l xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu = sizeFM (Branch xzw xzx xzy xzz yuu)

  
mkVBalBranch3Size_r xyx xyy xyz xzu xzv xzw xzx xzy xzz yuu = sizeFM (Branch xyx xyy xyz xzu xzv)

  
mkVBalBranch4 key elt fm_l EmptyFM = addToFM fm_l key elt
mkVBalBranch4 wwx wwy wwz wxu = mkVBalBranch3 wwx wwy wwz wxu

  
mkVBalBranch5 key elt EmptyFM fm_r = addToFM fm_r key elt
mkVBalBranch5 wxw wxx wxy wxz = mkVBalBranch4 wxw wxx wxy wxz

  sIZE_RATIO :: Int
sIZE_RATIO = Pos (Succ (Succ (Succ (Succ (Succ Zero)))))

  sizeFM :: FiniteMap b a  ->  Int
sizeFM EmptyFM = Pos Zero
sizeFM (Branch xw xx size xy xz) = size

  unitFM :: a  ->  b  ->  FiniteMap a b
unitFM key elt = Branch key elt (Pos (Succ Zero)) emptyFM emptyFM


module Maybe where
  import qualified FiniteMap
import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_glueBal2Mid_elt20(yuz1334, yuz1335, yuz1336, yuz1337, yuz1338, yuz1339, yuz1340, yuz1341, yuz1342, yuz1343, yuz1344, yuz1345, yuz1346, Branch(yuz13470, yuz13471, yuz13472, yuz13473, yuz13474), yuz1348, h, ba) → new_glueBal2Mid_elt20(yuz1334, yuz1335, yuz1336, yuz1337, yuz1338, yuz1339, yuz1340, yuz1341, yuz1342, yuz1343, yuz13470, yuz13471, yuz13472, yuz13473, yuz13474, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_glueBal2Mid_key20(yuz1318, yuz1319, yuz1320, yuz1321, yuz1322, yuz1323, yuz1324, yuz1325, yuz1326, yuz1327, yuz1328, yuz1329, yuz1330, Branch(yuz13310, yuz13311, yuz13312, yuz13313, yuz13314), yuz1332, h, ba) → new_glueBal2Mid_key20(yuz1318, yuz1319, yuz1320, yuz1321, yuz1322, yuz1323, yuz1324, yuz1325, yuz1326, yuz1327, yuz13310, yuz13311, yuz13312, yuz13313, yuz13314, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_glueBal2Mid_elt10(yuz1397, yuz1398, yuz1399, yuz1400, yuz1401, yuz1402, yuz1403, yuz1404, yuz1405, yuz1406, yuz1407, yuz1408, yuz1409, yuz1410, Branch(yuz14110, yuz14111, yuz14112, yuz14113, yuz14114), h, ba) → new_glueBal2Mid_elt10(yuz1397, yuz1398, yuz1399, yuz1400, yuz1401, yuz1402, yuz1403, yuz1404, yuz1405, yuz1406, yuz14110, yuz14111, yuz14112, yuz14113, yuz14114, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_glueBal2Mid_key10(yuz1381, yuz1382, yuz1383, yuz1384, yuz1385, yuz1386, yuz1387, yuz1388, yuz1389, yuz1390, yuz1391, yuz1392, yuz1393, yuz1394, Branch(yuz13950, yuz13951, yuz13952, yuz13953, yuz13954), h, ba) → new_glueBal2Mid_key10(yuz1381, yuz1382, yuz1383, yuz1384, yuz1385, yuz1386, yuz1387, yuz1388, yuz1389, yuz1390, yuz13950, yuz13951, yuz13952, yuz13953, yuz13954, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(Succ(yuz1194000), Succ(yuz1189000)) → new_esEs(yuz1194000, yuz1189000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(Succ(yuz23000), Succ(yuz1300000)) → new_esEs0(yuz23000, yuz1300000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(yuz121800), Succ(yuz121700)) → new_primMinusNat(yuz121800, yuz121700)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yuz11200), Succ(yuz600000)) → new_primPlusNat(yuz11200, yuz600000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yuz400000), yuz60000) → new_primMulNat(yuz400000, yuz60000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat0(Succ(yuz40000), Succ(yuz60000)) → new_primMulNat0(yuz40000, Succ(yuz60000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_addToFM_C2(yuz1189, yuz1190, yuz1191, Branch(yuz11920, yuz11921, yuz11922, yuz11923, yuz11924), yuz1193, yuz1194, yuz1195, True, h, ba) → new_addToFM_C2(yuz11920, yuz11921, yuz11922, yuz11923, yuz11924, yuz1194, yuz1195, new_lt(yuz1194, yuz11920, h), h, ba)
new_addToFM_C2(yuz1189, yuz1190, yuz1191, yuz1192, yuz1193, yuz1194, yuz1195, False, h, ba) → new_addToFM_C1(yuz1189, yuz1190, yuz1191, yuz1192, yuz1193, yuz1194, yuz1195, new_gt(yuz1194, yuz1189, h), h, ba)
new_addToFM_C1(yuz1209, yuz1210, yuz1211, yuz1212, yuz1213, yuz1214, yuz1215, True, bb, bc) → new_addToFM_C(yuz1213, yuz1214, yuz1215, bb, bc)
new_addToFM_C(Branch(yuz11920, yuz11921, yuz11922, yuz11923, yuz11924), yuz1194, yuz1195, h, ba) → new_addToFM_C2(yuz11920, yuz11921, yuz11922, yuz11923, yuz11924, yuz1194, yuz1195, new_lt(yuz1194, yuz11920, h), h, ba)

The TRS R consists of the following rules:

new_gt(yuz1194, yuz1189, ty_Int) → new_gt0(yuz1194, yuz1189)
new_esEs5 → False
new_gt(yuz1194, yuz1189, ty_Integer) → error([])
new_esEs12(yuz119400, Succ(yuz118900)) → new_esEs8(yuz119400, yuz118900)
new_esEs3(Zero, Zero) → new_esEs5
new_sr(Neg(yuz4000), Pos(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_sr(Pos(yuz4000), Neg(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_esEs8(Succ(yuz1194000), Succ(yuz1189000)) → new_esEs8(yuz1194000, yuz1189000)
new_esEs11(Neg(Succ(yuz119400)), Pos(yuz11890)) → new_esEs1
new_lt(yuz1194, yuz11920, app(app(app(ty_@3, be), bf), bg)) → error([])
new_esEs11(Pos(Zero), Neg(Succ(yuz118900))) → new_esEs9
new_esEs7(yuz21, yuz16) → new_esEs2(yuz21, yuz16)
new_lt(yuz1194, yuz11920, ty_Int) → new_lt0(yuz1194, yuz11920)
new_gt(yuz1194, yuz1189, app(ty_Maybe, bd)) → error([])
new_primPlusNat0(Succ(yuz11200), Succ(yuz600000)) → Succ(Succ(new_primPlusNat0(yuz11200, yuz600000)))
new_esEs2(Pos(Zero), Pos(Zero)) → new_esEs5
new_sr(Neg(yuz4000), Neg(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_esEs11(Pos(Zero), Neg(Zero)) → new_esEs10
new_esEs11(Neg(Zero), Pos(Zero)) → new_esEs10
new_primMulNat1(Succ(yuz40000), Succ(yuz60000)) → new_primPlusNat0(new_primMulNat1(yuz40000, Succ(yuz60000)), Succ(yuz60000))
new_esEs2(Neg(Zero), Pos(Succ(yuz1600))) → new_esEs6
new_primPlusNat0(Zero, Zero) → Zero
new_gt(yuz1194, yuz1189, ty_Double) → error([])
new_esEs10 → False
new_gt(yuz1194, yuz1189, app(app(app(ty_@3, be), bf), bg)) → error([])
new_lt(yuz1194, yuz11920, app(app(ty_Either, ca), cb)) → error([])
new_lt(yuz1194, yuz11920, app(app(ty_@2, cd), ce)) → error([])
new_gt(yuz1194, yuz1189, ty_Char) → error([])
new_lt(yuz1194, yuz11920, ty_Char) → error([])
new_gt(yuz1194, yuz1189, app(ty_[], cc)) → error([])
new_esEs2(Neg(Succ(yuz2100)), Neg(yuz160)) → new_esEs3(yuz160, Succ(yuz2100))
new_esEs11(Pos(Zero), Pos(Succ(yuz118900))) → new_esEs13(Zero, yuz118900)
new_gt(yuz1194, yuz1189, ty_Ordering) → error([])
new_gt(yuz1194, yuz1189, ty_@0) → error([])
new_gt(yuz1194, yuz1189, app(ty_Ratio, bh)) → error([])
new_esEs3(Succ(yuz23000), Zero) → new_esEs4
new_lt(yuz1194, yuz11920, app(ty_Ratio, bh)) → error([])
new_lt(yuz1194, yuz11920, ty_Ordering) → error([])
new_esEs11(Pos(Zero), Pos(Zero)) → new_esEs10
new_esEs13(Succ(yuz118900), yuz119400) → new_esEs8(yuz118900, yuz119400)
new_esEs9 → True
new_esEs8(Succ(yuz1194000), Zero) → new_esEs9
new_esEs11(Neg(Succ(yuz119400)), Neg(yuz11890)) → new_esEs13(yuz11890, yuz119400)
new_esEs3(Zero, Succ(yuz1300000)) → new_esEs6
new_lt(yuz1194, yuz11920, app(ty_Maybe, bd)) → error([])
new_gt(yuz1194, yuz1189, ty_Bool) → error([])
new_lt(yuz1194, yuz11920, ty_Integer) → error([])
new_esEs1 → False
new_esEs12(yuz119400, Zero) → new_esEs9
new_esEs3(Succ(yuz23000), Succ(yuz1300000)) → new_esEs3(yuz23000, yuz1300000)
new_esEs2(Pos(Succ(yuz2100)), Pos(yuz160)) → new_esEs3(Succ(yuz2100), yuz160)
new_esEs11(Neg(Zero), Neg(Zero)) → new_esEs10
new_esEs13(Zero, yuz119400) → new_esEs1
new_esEs8(Zero, Succ(yuz1189000)) → new_esEs1
new_lt1(Float(yuz400, yuz401), Float(yuz600, yuz601)) → new_esEs7(new_sr(yuz400, yuz600), new_sr(yuz401, yuz601))
new_esEs4 → False
new_esEs2(Neg(Zero), Neg(Zero)) → new_esEs5
new_lt(yuz1194, yuz11920, ty_Bool) → error([])
new_esEs11(Neg(Zero), Pos(Succ(yuz118900))) → new_esEs1
new_lt(yuz1194, yuz11920, ty_Float) → new_lt1(yuz1194, yuz11920)
new_esEs8(Zero, Zero) → new_esEs10
new_lt(yuz1194, yuz11920, app(ty_[], cc)) → error([])
new_esEs2(Neg(Zero), Neg(Succ(yuz1600))) → new_esEs3(Succ(yuz1600), Zero)
new_esEs2(Neg(Succ(yuz2100)), Pos(yuz160)) → new_esEs6
new_esEs2(Pos(Zero), Neg(Succ(yuz1600))) → new_esEs4
new_sr(Pos(yuz4000), Pos(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_gt(Float(yuz11940, yuz11941), Float(yuz11890, yuz11891), ty_Float) → new_esEs11(new_sr(yuz11940, yuz11890), new_sr(yuz11941, yuz11891))
new_esEs11(Pos(Succ(yuz119400)), Pos(yuz11890)) → new_esEs12(yuz119400, yuz11890)
new_gt(yuz1194, yuz1189, app(app(ty_@2, cd), ce)) → error([])
new_esEs2(Pos(Zero), Pos(Succ(yuz1600))) → new_esEs3(Zero, Succ(yuz1600))
new_esEs2(Pos(Succ(yuz2100)), Neg(yuz160)) → new_esEs4
new_esEs2(Neg(Zero), Pos(Zero)) → new_esEs5
new_esEs2(Pos(Zero), Neg(Zero)) → new_esEs5
new_esEs11(Pos(Succ(yuz119400)), Neg(yuz11890)) → new_esEs9
new_lt0(yuz21, yuz16) → new_esEs7(yuz21, yuz16)
new_gt0(yuz1194, yuz1189) → new_esEs11(yuz1194, yuz1189)
new_esEs6 → True
new_primPlusNat0(Zero, Succ(yuz600000)) → Succ(yuz600000)
new_primPlusNat0(Succ(yuz11200), Zero) → Succ(yuz11200)
new_lt(yuz1194, yuz11920, ty_@0) → error([])
new_primMulNat1(Succ(yuz40000), Zero) → Zero
new_primMulNat1(Zero, Succ(yuz60000)) → Zero
new_primMulNat1(Zero, Zero) → Zero
new_lt(yuz1194, yuz11920, ty_Double) → error([])
new_gt(yuz1194, yuz1189, app(app(ty_Either, ca), cb)) → error([])
new_esEs11(Neg(Zero), Neg(Succ(yuz118900))) → new_esEs12(yuz118900, Zero)

The set Q consists of the following terms:

new_lt(x0, x1, ty_Float)
new_esEs12(x0, Zero)
new_esEs13(Succ(x0), x1)
new_gt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_gt(x0, x1, app(app(ty_@2, x2), x3))
new_lt(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Succ(x0), Zero)
new_esEs2(Neg(Succ(x0)), Neg(x1))
new_gt0(x0, x1)
new_primMulNat1(Zero, Succ(x0))
new_lt(x0, x1, app(app(ty_Either, x2), x3))
new_gt(x0, x1, ty_Bool)
new_esEs3(Succ(x0), Succ(x1))
new_esEs8(Zero, Zero)
new_esEs4
new_lt(x0, x1, ty_Char)
new_gt(x0, x1, ty_Integer)
new_esEs3(Zero, Succ(x0))
new_lt(x0, x1, ty_@0)
new_esEs5
new_esEs11(Pos(Succ(x0)), Pos(x1))
new_lt(x0, x1, ty_Int)
new_gt(x0, x1, app(ty_Ratio, x2))
new_lt(x0, x1, app(ty_Ratio, x2))
new_primMulNat1(Succ(x0), Zero)
new_esEs2(Neg(Zero), Pos(Zero))
new_esEs2(Pos(Zero), Neg(Zero))
new_esEs8(Zero, Succ(x0))
new_gt(x0, x1, app(ty_Maybe, x2))
new_sr(Pos(x0), Pos(x1))
new_lt(x0, x1, ty_Ordering)
new_gt(x0, x1, app(app(ty_Either, x2), x3))
new_esEs13(Zero, x0)
new_esEs7(x0, x1)
new_gt(x0, x1, app(ty_[], x2))
new_primPlusNat0(Zero, Zero)
new_esEs2(Pos(Succ(x0)), Pos(x1))
new_lt(x0, x1, ty_Bool)
new_lt(x0, x1, ty_Double)
new_primPlusNat0(Zero, Succ(x0))
new_esEs11(Pos(Zero), Pos(Succ(x0)))
new_esEs3(Succ(x0), Zero)
new_lt(x0, x1, app(ty_[], x2))
new_gt(x0, x1, ty_@0)
new_esEs11(Neg(Succ(x0)), Neg(x1))
new_primMulNat1(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_gt(x0, x1, ty_Double)
new_gt(x0, x1, ty_Char)
new_primPlusNat0(Succ(x0), Zero)
new_esEs2(Pos(Zero), Pos(Zero))
new_gt(x0, x1, ty_Ordering)
new_gt(x0, x1, ty_Int)
new_esEs12(x0, Succ(x1))
new_esEs8(Succ(x0), Succ(x1))
new_esEs1
new_esEs2(Neg(Zero), Neg(Succ(x0)))
new_esEs11(Pos(Zero), Pos(Zero))
new_lt(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_lt1(Float(x0, x1), Float(x2, x3))
new_esEs11(Neg(Zero), Neg(Zero))
new_esEs11(Pos(Zero), Neg(Zero))
new_esEs11(Neg(Zero), Pos(Zero))
new_lt0(x0, x1)
new_esEs2(Pos(Succ(x0)), Neg(x1))
new_esEs2(Neg(Succ(x0)), Pos(x1))
new_primMulNat1(Succ(x0), Succ(x1))
new_esEs11(Neg(Zero), Neg(Succ(x0)))
new_sr(Neg(x0), Neg(x1))
new_esEs2(Pos(Zero), Neg(Succ(x0)))
new_esEs2(Neg(Zero), Pos(Succ(x0)))
new_esEs2(Neg(Zero), Neg(Zero))
new_lt(x0, x1, ty_Integer)
new_gt(Float(x0, x1), Float(x2, x3), ty_Float)
new_esEs10
new_esEs9
new_esEs11(Pos(Succ(x0)), Neg(x1))
new_esEs3(Zero, Zero)
new_esEs11(Neg(Succ(x0)), Pos(x1))
new_lt(x0, x1, app(ty_Maybe, x2))
new_esEs11(Neg(Zero), Pos(Succ(x0)))
new_esEs11(Pos(Zero), Neg(Succ(x0)))
new_esEs6
new_esEs2(Pos(Zero), Pos(Succ(x0)))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_mkVBalBranch3MkVBalBranch2(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, False, h, ba) → new_mkVBalBranch3MkVBalBranch1(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, new_lt0(new_sr0(new_mkVBalBranch3Size_r(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), new_mkVBalBranch3Size_l(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch1(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, Branch(yuz2040, yuz2041, yuz2042, yuz2043, yuz2044), yuz21, yuz22, True, h, ba) → new_mkVBalBranch3(yuz21, yuz22, yuz2040, yuz2041, yuz2042, yuz2043, yuz2044, yuz140, yuz141, yuz142, yuz143, yuz144, h, ba)
new_mkVBalBranch3(yuz21, yuz22, yuz200, yuz201, yuz202, yuz203, yuz204, yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, h, ba) → new_mkVBalBranch3MkVBalBranch2(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, new_lt0(new_sr(new_sIZE_RATIO, new_mkVBalBranch3Size_l(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), new_mkVBalBranch3Size_r(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch2(yuz140, yuz141, yuz142, Branch(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434), yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, True, h, ba) → new_mkVBalBranch3MkVBalBranch2(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, new_lt0(new_sr(new_sIZE_RATIO, new_mkVBalBranch3Size_l(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), new_mkVBalBranch3Size_r(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), h, ba)

The TRS R consists of the following rules:

new_mkVBalBranch3Size_r(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba) → new_sizeFM(Branch(yuz140, yuz141, yuz142, yuz143, yuz144), h, ba)
new_primPlusNat1(Succ(yuz1120), yuz60000) → Succ(Succ(new_primPlusNat0(yuz1120, yuz60000)))
new_esEs5 → False
new_esEs3(Zero, Succ(yuz1300000)) → new_esEs6
new_sr0(Neg(yuz11770)) → Neg(new_primMulNat2(yuz11770))
new_sr(Neg(yuz4000), Pos(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_sr(Pos(yuz4000), Neg(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_esEs3(Zero, Zero) → new_esEs5
new_esEs3(Succ(yuz23000), Succ(yuz1300000)) → new_esEs3(yuz23000, yuz1300000)
new_mkVBalBranch3Size_l(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba) → new_sizeFM0(yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)
new_primPlusNat1(Zero, yuz60000) → Succ(yuz60000)
new_primMulNat3(Zero, yuz60000) → Zero
new_sizeFM0(yuz200, yuz201, yuz202, yuz203, yuz204, h, ba) → yuz202
new_esEs7(yuz21, yuz16) → new_esEs2(yuz21, yuz16)
new_esEs2(Pos(Succ(yuz2100)), Pos(yuz160)) → new_esEs3(Succ(yuz2100), yuz160)
new_primMulNat2(Zero) → Zero
new_primPlusNat0(Succ(yuz11200), Succ(yuz600000)) → Succ(Succ(new_primPlusNat0(yuz11200, yuz600000)))
new_esEs4 → False
new_sIZE_RATIO → Pos(Succ(Succ(Succ(Succ(Succ(Zero))))))
new_esEs2(Pos(Zero), Pos(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Neg(Zero)) → new_esEs5
new_sr0(Pos(yuz11770)) → Pos(new_primMulNat2(yuz11770))
new_primMulNat2(Succ(yuz117700)) → new_primPlusNat0(new_primMulNat3(Succ(Succ(Succ(Succ(Zero)))), yuz117700), Succ(yuz117700))
new_primMulNat3(Succ(yuz400000), yuz60000) → new_primPlusNat1(new_primMulNat3(yuz400000, yuz60000), yuz60000)
new_sr(Neg(yuz4000), Neg(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_primMulNat1(Succ(yuz40000), Succ(yuz60000)) → new_primPlusNat0(new_primMulNat1(yuz40000, Succ(yuz60000)), Succ(yuz60000))
new_esEs2(Neg(Zero), Pos(Succ(yuz1600))) → new_esEs6
new_primPlusNat0(Zero, Zero) → Zero
new_esEs2(Pos(Zero), Neg(Succ(yuz1600))) → new_esEs4
new_esEs2(Neg(Succ(yuz2100)), Pos(yuz160)) → new_esEs6
new_esEs2(Neg(Zero), Neg(Succ(yuz1600))) → new_esEs3(Succ(yuz1600), Zero)
new_sr(Pos(yuz4000), Pos(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_esEs2(Pos(Succ(yuz2100)), Neg(yuz160)) → new_esEs4
new_esEs2(Pos(Zero), Pos(Succ(yuz1600))) → new_esEs3(Zero, Succ(yuz1600))
new_esEs2(Pos(Zero), Neg(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Pos(Zero)) → new_esEs5
new_lt0(yuz21, yuz16) → new_esEs7(yuz21, yuz16)
new_sizeFM(EmptyFM, h, ba) → Pos(Zero)
new_esEs6 → True
new_esEs2(Neg(Succ(yuz2100)), Neg(yuz160)) → new_esEs3(yuz160, Succ(yuz2100))
new_primPlusNat0(Succ(yuz11200), Zero) → Succ(yuz11200)
new_primPlusNat0(Zero, Succ(yuz600000)) → Succ(yuz600000)
new_primMulNat1(Succ(yuz40000), Zero) → Zero
new_primMulNat1(Zero, Succ(yuz60000)) → Zero
new_primMulNat1(Zero, Zero) → Zero
new_esEs3(Succ(yuz23000), Zero) → new_esEs4
new_sizeFM(Branch(yuz11660, yuz11661, yuz11662, yuz11663, yuz11664), h, ba) → yuz11662

The set Q consists of the following terms:

new_esEs3(Succ(x0), Zero)
new_sr0(Neg(x0))
new_primMulNat1(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primPlusNat1(Zero, x0)
new_primMulNat2(Succ(x0))
new_sizeFM(EmptyFM, x0, x1)
new_primMulNat2(Zero)
new_esEs2(Neg(Succ(x0)), Neg(x1))
new_primPlusNat0(Succ(x0), Zero)
new_esEs2(Pos(Zero), Pos(Zero))
new_primMulNat1(Zero, Succ(x0))
new_esEs3(Succ(x0), Succ(x1))
new_esEs4
new_esEs3(Zero, Succ(x0))
new_esEs5
new_mkVBalBranch3Size_r(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_primMulNat3(Succ(x0), x1)
new_esEs2(Neg(Zero), Neg(Succ(x0)))
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_mkVBalBranch3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_sr0(Pos(x0))
new_primMulNat1(Succ(x0), Zero)
new_esEs2(Pos(Zero), Neg(Zero))
new_esEs2(Neg(Zero), Pos(Zero))
new_sr(Pos(x0), Pos(x1))
new_lt0(x0, x1)
new_esEs2(Pos(Succ(x0)), Neg(x1))
new_esEs2(Neg(Succ(x0)), Pos(x1))
new_primMulNat1(Succ(x0), Succ(x1))
new_esEs7(x0, x1)
new_sr(Neg(x0), Neg(x1))
new_esEs2(Pos(Zero), Neg(Succ(x0)))
new_esEs2(Neg(Zero), Pos(Succ(x0)))
new_esEs2(Neg(Zero), Neg(Zero))
new_primMulNat3(Zero, x0)
new_primPlusNat0(Zero, Zero)
new_esEs3(Zero, Zero)
new_esEs2(Pos(Succ(x0)), Pos(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Succ(x0))
new_sIZE_RATIO
new_esEs6
new_esEs2(Pos(Zero), Pos(Succ(x0)))
new_sizeFM0(x0, x1, x2, x3, x4, x5, x6)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_mkVBalBranch3MkVBalBranch2(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, False, h, ba) → new_mkVBalBranch3MkVBalBranch1(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, new_lt0(new_sr0(new_mkVBalBranch3Size_r(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), new_mkVBalBranch3Size_l(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch1(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, Branch(yuz2040, yuz2041, yuz2042, yuz2043, yuz2044), yuz21, yuz22, True, h, ba) → new_mkVBalBranch3(yuz21, yuz22, yuz2040, yuz2041, yuz2042, yuz2043, yuz2044, yuz140, yuz141, yuz142, yuz143, yuz144, h, ba)
new_mkVBalBranch3(yuz21, yuz22, yuz200, yuz201, yuz202, yuz203, yuz204, yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, h, ba) → new_mkVBalBranch3MkVBalBranch2(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, new_lt0(new_sr(new_sIZE_RATIO, new_mkVBalBranch3Size_l(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), new_mkVBalBranch3Size_r(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), h, ba)
new_mkVBalBranch3MkVBalBranch2(yuz140, yuz141, yuz142, Branch(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434), yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, True, h, ba) → new_mkVBalBranch3MkVBalBranch2(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, yuz21, yuz22, new_lt0(new_sr(new_sIZE_RATIO, new_mkVBalBranch3Size_l(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), new_mkVBalBranch3Size_r(yuz1430, yuz1431, yuz1432, yuz1433, yuz1434, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)), h, ba)

The TRS R consists of the following rules:

new_sIZE_RATIO → Pos(Succ(Succ(Succ(Succ(Succ(Zero))))))
new_mkVBalBranch3Size_l(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba) → new_sizeFM0(yuz200, yuz201, yuz202, yuz203, yuz204, h, ba)
new_sr(Neg(yuz4000), Pos(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_sr(Pos(yuz4000), Neg(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_sr(Neg(yuz4000), Neg(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_sr(Pos(yuz4000), Pos(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_mkVBalBranch3Size_r(yuz140, yuz141, yuz142, yuz143, yuz144, yuz200, yuz201, yuz202, yuz203, yuz204, h, ba) → new_sizeFM(Branch(yuz140, yuz141, yuz142, yuz143, yuz144), h, ba)
new_lt0(yuz21, yuz16) → new_esEs7(yuz21, yuz16)
new_esEs7(yuz21, yuz16) → new_esEs2(yuz21, yuz16)
new_esEs2(Pos(Succ(yuz2100)), Pos(yuz160)) → new_esEs3(Succ(yuz2100), yuz160)
new_esEs2(Pos(Zero), Pos(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Neg(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Pos(Succ(yuz1600))) → new_esEs6
new_esEs2(Pos(Zero), Neg(Succ(yuz1600))) → new_esEs4
new_esEs2(Neg(Succ(yuz2100)), Pos(yuz160)) → new_esEs6
new_esEs2(Neg(Zero), Neg(Succ(yuz1600))) → new_esEs3(Succ(yuz1600), Zero)
new_esEs2(Pos(Succ(yuz2100)), Neg(yuz160)) → new_esEs4
new_esEs2(Pos(Zero), Pos(Succ(yuz1600))) → new_esEs3(Zero, Succ(yuz1600))
new_esEs2(Pos(Zero), Neg(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Pos(Zero)) → new_esEs5
new_esEs2(Neg(Succ(yuz2100)), Neg(yuz160)) → new_esEs3(yuz160, Succ(yuz2100))
new_esEs3(Zero, Succ(yuz1300000)) → new_esEs6
new_esEs3(Succ(yuz23000), Succ(yuz1300000)) → new_esEs3(yuz23000, yuz1300000)
new_esEs3(Zero, Zero) → new_esEs5
new_esEs3(Succ(yuz23000), Zero) → new_esEs4
new_esEs4 → False
new_esEs5 → False
new_esEs6 → True
new_sizeFM(Branch(yuz11660, yuz11661, yuz11662, yuz11663, yuz11664), h, ba) → yuz11662
new_primMulNat1(Succ(yuz40000), Succ(yuz60000)) → new_primPlusNat0(new_primMulNat1(yuz40000, Succ(yuz60000)), Succ(yuz60000))
new_primMulNat1(Succ(yuz40000), Zero) → Zero
new_primMulNat1(Zero, Succ(yuz60000)) → Zero
new_primMulNat1(Zero, Zero) → Zero
new_primPlusNat0(Succ(yuz11200), Succ(yuz600000)) → Succ(Succ(new_primPlusNat0(yuz11200, yuz600000)))
new_primPlusNat0(Zero, Succ(yuz600000)) → Succ(yuz600000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(yuz11200), Zero) → Succ(yuz11200)
new_sizeFM0(yuz200, yuz201, yuz202, yuz203, yuz204, h, ba) → yuz202
new_sr0(Neg(yuz11770)) → Neg(new_primMulNat2(yuz11770))
new_sr0(Pos(yuz11770)) → Pos(new_primMulNat2(yuz11770))
new_primMulNat2(Zero) → Zero
new_primMulNat2(Succ(yuz117700)) → new_primPlusNat0(new_primMulNat3(Succ(Succ(Succ(Succ(Zero)))), yuz117700), Succ(yuz117700))
new_primMulNat3(Succ(yuz400000), yuz60000) → new_primPlusNat1(new_primMulNat3(yuz400000, yuz60000), yuz60000)
new_primMulNat3(Zero, yuz60000) → Zero
new_primPlusNat1(Succ(yuz1120), yuz60000) → Succ(Succ(new_primPlusNat0(yuz1120, yuz60000)))
new_primPlusNat1(Zero, yuz60000) → Succ(yuz60000)

The set Q consists of the following terms:

new_esEs3(Succ(x0), Zero)
new_sr0(Neg(x0))
new_primMulNat1(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primPlusNat1(Zero, x0)
new_primMulNat2(Succ(x0))
new_sizeFM(EmptyFM, x0, x1)
new_primMulNat2(Zero)
new_esEs2(Neg(Succ(x0)), Neg(x1))
new_primPlusNat0(Succ(x0), Zero)
new_esEs2(Pos(Zero), Pos(Zero))
new_primMulNat1(Zero, Succ(x0))
new_esEs3(Succ(x0), Succ(x1))
new_esEs4
new_esEs3(Zero, Succ(x0))
new_esEs5
new_mkVBalBranch3Size_r(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_primMulNat3(Succ(x0), x1)
new_esEs2(Neg(Zero), Neg(Succ(x0)))
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_mkVBalBranch3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_sr0(Pos(x0))
new_primMulNat1(Succ(x0), Zero)
new_esEs2(Pos(Zero), Neg(Zero))
new_esEs2(Neg(Zero), Pos(Zero))
new_sr(Pos(x0), Pos(x1))
new_lt0(x0, x1)
new_esEs2(Pos(Succ(x0)), Neg(x1))
new_esEs2(Neg(Succ(x0)), Pos(x1))
new_primMulNat1(Succ(x0), Succ(x1))
new_esEs7(x0, x1)
new_sr(Neg(x0), Neg(x1))
new_esEs2(Pos(Zero), Neg(Succ(x0)))
new_esEs2(Neg(Zero), Pos(Succ(x0)))
new_esEs2(Neg(Zero), Neg(Zero))
new_primMulNat3(Zero, x0)
new_primPlusNat0(Zero, Zero)
new_esEs3(Zero, Zero)
new_esEs2(Pos(Succ(x0)), Pos(x1))
new_primPlusNat1(Succ(x0), x1)
new_primPlusNat0(Zero, Succ(x0))
new_sIZE_RATIO
new_esEs6
new_esEs2(Pos(Zero), Pos(Succ(x0)))
new_sizeFM0(x0, x1, x2, x3, x4, x5, x6)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteMin(yuz290, yuz291, yuz292, Branch(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934), yuz294, h, ba) → new_deleteMin(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteMax(yuz350, yuz351, yuz352, yuz353, Branch(yuz3540, yuz3541, yuz3542, yuz3543, yuz3544), h, ba) → new_deleteMax(yuz3540, yuz3541, yuz3542, yuz3543, yuz3544, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_glueVBal3GlueVBal2(yuz290, yuz291, yuz292, Branch(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934), yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, True, h, ba) → new_glueVBal3GlueVBal2(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, new_lt0(new_sr(new_sIZE_RATIO, new_glueVBal3Size_l(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), new_glueVBal3Size_r(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), h, ba)
new_glueVBal3GlueVBal1(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, Branch(yuz3540, yuz3541, yuz3542, yuz3543, yuz3544), True, h, ba) → new_glueVBal3(yuz3540, yuz3541, yuz3542, yuz3543, yuz3544, yuz290, yuz291, yuz292, yuz293, yuz294, h, ba)
new_glueVBal3GlueVBal2(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, False, h, ba) → new_glueVBal3GlueVBal1(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, new_lt0(new_sr(new_sIZE_RATIO, new_glueVBal3Size_r(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), new_glueVBal3Size_l(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), h, ba)
new_glueVBal3(yuz350, yuz351, yuz352, yuz353, yuz354, yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, h, ba) → new_glueVBal3GlueVBal2(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, new_lt0(new_sr(new_sIZE_RATIO, new_glueVBal3Size_l(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), new_glueVBal3Size_r(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), h, ba)

The TRS R consists of the following rules:

new_esEs5 → False
new_esEs3(Zero, Succ(yuz1300000)) → new_esEs6
new_sr(Neg(yuz4000), Pos(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_sr(Pos(yuz4000), Neg(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_esEs3(Zero, Zero) → new_esEs5
new_esEs3(Succ(yuz23000), Succ(yuz1300000)) → new_esEs3(yuz23000, yuz1300000)
new_esEs7(yuz21, yuz16) → new_esEs2(yuz21, yuz16)
new_esEs2(Pos(Succ(yuz2100)), Pos(yuz160)) → new_esEs3(Succ(yuz2100), yuz160)
new_primPlusNat0(Succ(yuz11200), Succ(yuz600000)) → Succ(Succ(new_primPlusNat0(yuz11200, yuz600000)))
new_esEs4 → False
new_sIZE_RATIO → Pos(Succ(Succ(Succ(Succ(Succ(Zero))))))
new_esEs2(Pos(Zero), Pos(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Neg(Zero)) → new_esEs5
new_sr(Neg(yuz4000), Neg(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_primMulNat1(Succ(yuz40000), Succ(yuz60000)) → new_primPlusNat0(new_primMulNat1(yuz40000, Succ(yuz60000)), Succ(yuz60000))
new_esEs2(Neg(Zero), Pos(Succ(yuz1600))) → new_esEs6
new_primPlusNat0(Zero, Zero) → Zero
new_esEs2(Pos(Zero), Neg(Succ(yuz1600))) → new_esEs4
new_esEs2(Neg(Succ(yuz2100)), Pos(yuz160)) → new_esEs6
new_esEs2(Neg(Zero), Neg(Succ(yuz1600))) → new_esEs3(Succ(yuz1600), Zero)
new_sr(Pos(yuz4000), Pos(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_glueVBal3Size_r(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba) → new_sizeFM(Branch(yuz290, yuz291, yuz292, yuz293, yuz294), h, ba)
new_esEs2(Pos(Succ(yuz2100)), Neg(yuz160)) → new_esEs4
new_esEs2(Pos(Zero), Pos(Succ(yuz1600))) → new_esEs3(Zero, Succ(yuz1600))
new_esEs2(Pos(Zero), Neg(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Pos(Zero)) → new_esEs5
new_glueVBal3Size_l(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba) → new_sizeFM(Branch(yuz350, yuz351, yuz352, yuz353, yuz354), h, ba)
new_lt0(yuz21, yuz16) → new_esEs7(yuz21, yuz16)
new_sizeFM(EmptyFM, bb, bc) → Pos(Zero)
new_esEs6 → True
new_esEs2(Neg(Succ(yuz2100)), Neg(yuz160)) → new_esEs3(yuz160, Succ(yuz2100))
new_primPlusNat0(Succ(yuz11200), Zero) → Succ(yuz11200)
new_primPlusNat0(Zero, Succ(yuz600000)) → Succ(yuz600000)
new_primMulNat1(Succ(yuz40000), Zero) → Zero
new_primMulNat1(Zero, Succ(yuz60000)) → Zero
new_primMulNat1(Zero, Zero) → Zero
new_esEs3(Succ(yuz23000), Zero) → new_esEs4
new_sizeFM(Branch(yuz11660, yuz11661, yuz11662, yuz11663, yuz11664), bb, bc) → yuz11662

The set Q consists of the following terms:

new_esEs3(Succ(x0), Zero)
new_primMulNat1(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_sizeFM(EmptyFM, x0, x1)
new_esEs2(Neg(Succ(x0)), Neg(x1))
new_primPlusNat0(Succ(x0), Zero)
new_esEs2(Pos(Zero), Pos(Zero))
new_primMulNat1(Zero, Succ(x0))
new_esEs3(Succ(x0), Succ(x1))
new_esEs4
new_esEs3(Zero, Succ(x0))
new_glueVBal3Size_r(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs5
new_esEs2(Neg(Zero), Neg(Succ(x0)))
new_glueVBal3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_primMulNat1(Succ(x0), Zero)
new_esEs2(Pos(Zero), Neg(Zero))
new_esEs2(Neg(Zero), Pos(Zero))
new_sr(Pos(x0), Pos(x1))
new_lt0(x0, x1)
new_esEs2(Neg(Succ(x0)), Pos(x1))
new_esEs2(Pos(Succ(x0)), Neg(x1))
new_primMulNat1(Succ(x0), Succ(x1))
new_esEs7(x0, x1)
new_sr(Neg(x0), Neg(x1))
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_esEs2(Neg(Zero), Pos(Succ(x0)))
new_esEs2(Pos(Zero), Neg(Succ(x0)))
new_esEs2(Neg(Zero), Neg(Zero))
new_esEs3(Zero, Zero)
new_primPlusNat0(Zero, Zero)
new_esEs2(Pos(Succ(x0)), Pos(x1))
new_primPlusNat0(Zero, Succ(x0))
new_sIZE_RATIO
new_esEs6
new_esEs2(Pos(Zero), Pos(Succ(x0)))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ UsableRulesProof
                                  ↳ QDP
                                    ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_glueVBal3GlueVBal2(yuz290, yuz291, yuz292, Branch(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934), yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, True, h, ba) → new_glueVBal3GlueVBal2(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, new_lt0(new_sr(new_sIZE_RATIO, new_glueVBal3Size_l(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), new_glueVBal3Size_r(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), h, ba)
new_glueVBal3GlueVBal1(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, Branch(yuz3540, yuz3541, yuz3542, yuz3543, yuz3544), True, h, ba) → new_glueVBal3(yuz3540, yuz3541, yuz3542, yuz3543, yuz3544, yuz290, yuz291, yuz292, yuz293, yuz294, h, ba)
new_glueVBal3GlueVBal2(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, False, h, ba) → new_glueVBal3GlueVBal1(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, new_lt0(new_sr(new_sIZE_RATIO, new_glueVBal3Size_r(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), new_glueVBal3Size_l(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), h, ba)
new_glueVBal3(yuz350, yuz351, yuz352, yuz353, yuz354, yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, h, ba) → new_glueVBal3GlueVBal2(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, new_lt0(new_sr(new_sIZE_RATIO, new_glueVBal3Size_l(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), new_glueVBal3Size_r(yuz2930, yuz2931, yuz2932, yuz2933, yuz2934, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba)), h, ba)

The TRS R consists of the following rules:

new_sIZE_RATIO → Pos(Succ(Succ(Succ(Succ(Succ(Zero))))))
new_glueVBal3Size_l(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba) → new_sizeFM(Branch(yuz350, yuz351, yuz352, yuz353, yuz354), h, ba)
new_sr(Neg(yuz4000), Pos(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_sr(Pos(yuz4000), Neg(yuz6000)) → Neg(new_primMulNat1(yuz4000, yuz6000))
new_sr(Neg(yuz4000), Neg(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_sr(Pos(yuz4000), Pos(yuz6000)) → Pos(new_primMulNat1(yuz4000, yuz6000))
new_glueVBal3Size_r(yuz290, yuz291, yuz292, yuz293, yuz294, yuz350, yuz351, yuz352, yuz353, yuz354, h, ba) → new_sizeFM(Branch(yuz290, yuz291, yuz292, yuz293, yuz294), h, ba)
new_lt0(yuz21, yuz16) → new_esEs7(yuz21, yuz16)
new_esEs7(yuz21, yuz16) → new_esEs2(yuz21, yuz16)
new_esEs2(Pos(Succ(yuz2100)), Pos(yuz160)) → new_esEs3(Succ(yuz2100), yuz160)
new_esEs2(Pos(Zero), Pos(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Neg(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Pos(Succ(yuz1600))) → new_esEs6
new_esEs2(Pos(Zero), Neg(Succ(yuz1600))) → new_esEs4
new_esEs2(Neg(Succ(yuz2100)), Pos(yuz160)) → new_esEs6
new_esEs2(Neg(Zero), Neg(Succ(yuz1600))) → new_esEs3(Succ(yuz1600), Zero)
new_esEs2(Pos(Succ(yuz2100)), Neg(yuz160)) → new_esEs4
new_esEs2(Pos(Zero), Pos(Succ(yuz1600))) → new_esEs3(Zero, Succ(yuz1600))
new_esEs2(Pos(Zero), Neg(Zero)) → new_esEs5
new_esEs2(Neg(Zero), Pos(Zero)) → new_esEs5
new_esEs2(Neg(Succ(yuz2100)), Neg(yuz160)) → new_esEs3(yuz160, Succ(yuz2100))
new_esEs3(Zero, Succ(yuz1300000)) → new_esEs6
new_esEs3(Succ(yuz23000), Succ(yuz1300000)) → new_esEs3(yuz23000, yuz1300000)
new_esEs3(Zero, Zero) → new_esEs5
new_esEs3(Succ(yuz23000), Zero) → new_esEs4
new_esEs4 → False
new_esEs5 → False
new_esEs6 → True
new_sizeFM(Branch(yuz11660, yuz11661, yuz11662, yuz11663, yuz11664), bb, bc) → yuz11662
new_primMulNat1(Succ(yuz40000), Succ(yuz60000)) → new_primPlusNat0(new_primMulNat1(yuz40000, Succ(yuz60000)), Succ(yuz60000))
new_primMulNat1(Succ(yuz40000), Zero) → Zero
new_primMulNat1(Zero, Succ(yuz60000)) → Zero
new_primMulNat1(Zero, Zero) → Zero
new_primPlusNat0(Succ(yuz11200), Succ(yuz600000)) → Succ(Succ(new_primPlusNat0(yuz11200, yuz600000)))
new_primPlusNat0(Zero, Succ(yuz600000)) → Succ(yuz600000)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(yuz11200), Zero) → Succ(yuz11200)

The set Q consists of the following terms:

new_esEs3(Succ(x0), Zero)
new_primMulNat1(Zero, Zero)
new_primPlusNat0(Succ(x0), Succ(x1))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_sizeFM(EmptyFM, x0, x1)
new_esEs2(Neg(Succ(x0)), Neg(x1))
new_primPlusNat0(Succ(x0), Zero)
new_esEs2(Pos(Zero), Pos(Zero))
new_primMulNat1(Zero, Succ(x0))
new_esEs3(Succ(x0), Succ(x1))
new_esEs4
new_esEs3(Zero, Succ(x0))
new_glueVBal3Size_r(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_esEs5
new_esEs2(Neg(Zero), Neg(Succ(x0)))
new_glueVBal3Size_l(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
new_primMulNat1(Succ(x0), Zero)
new_esEs2(Pos(Zero), Neg(Zero))
new_esEs2(Neg(Zero), Pos(Zero))
new_sr(Pos(x0), Pos(x1))
new_lt0(x0, x1)
new_esEs2(Neg(Succ(x0)), Pos(x1))
new_esEs2(Pos(Succ(x0)), Neg(x1))
new_primMulNat1(Succ(x0), Succ(x1))
new_esEs7(x0, x1)
new_sr(Neg(x0), Neg(x1))
new_sizeFM(Branch(x0, x1, x2, x3, x4), x5, x6)
new_esEs2(Neg(Zero), Pos(Succ(x0)))
new_esEs2(Pos(Zero), Neg(Succ(x0)))
new_esEs2(Neg(Zero), Neg(Zero))
new_esEs3(Zero, Zero)
new_primPlusNat0(Zero, Zero)
new_esEs2(Pos(Succ(x0)), Pos(x1))
new_primPlusNat0(Zero, Succ(x0))
new_sIZE_RATIO
new_esEs6
new_esEs2(Pos(Zero), Pos(Succ(x0)))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ BR
            ↳ HASKELL
              ↳ COR
                ↳ HASKELL
                  ↳ LetRed
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_filterFM1(yuz3, yuz40, yuz41, yuz42, yuz43, yuz44, h) → new_filterFM(yuz3, yuz44, h)
new_filterFM1(yuz3, yuz40, yuz41, yuz42, yuz43, yuz44, h) → new_filterFM(yuz3, yuz43, h)
new_filterFM(yuz3, Branch(yuz40, yuz41, yuz42, yuz43, yuz44), h) → new_filterFM1(yuz3, yuz40, yuz41, yuz42, yuz43, yuz44, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: